Theorem 3eqtrrd 1930

Description: A deduction from three chained equalities. (The proof was shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtrd.1	|- (ph -> A = B)
3eqtrd.2	|- (ph -> B = C)
3eqtrd.3	|- (ph -> C = D)

Assertion

Ref	Expression
3eqtrrd	|- (ph -> D = A)

Proof of Theorem 3eqtrrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. . 3 |- (ph -> A = B)
2		3eqtrd.2	. . 3 |- (ph -> B = C)
3	1, 2	eqtrd 1925	. 2 |- (ph -> A = C)
4		3eqtrd.3	. 2 |- (ph -> C = D)
5	3, 4	eqtr2d 1926	1 |- (ph -> D = A)

Syntax hints:   -> wi 3   = wceq 1298

This theorem is referenced by:  axcnre 6439  seq1seq02 7786  seqzp1 7791  expubnd 7853  subsq 7888  rereb 8026  sincossq 8726  efieq1re 8751  abssinper 10062  upxp 10225  nmbdoplbi 11586  nmcopexlem3 11590  nmcoplbi 11595  nmbdfnlbi 11615  nmcfnexlem3 11619  nmcfnlbi 11624  hstoh 11804  eucalg 13755  fprodneg 14741  ismrer1 16024

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain