Theorem 3eqtrrd 2125

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof 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 2120	. 2 |- ( ph -> A = C )
4		3eqtrd.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtr2d 2121	1 |- ( ph -> D = A )

Syntax hints:   -> wi 4   = wceq 1289

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081

This theorem is referenced by:  nnanq0  7007  1idprl  7139  1idpru  7140  axcnre  7406  fseq1p1m1  9496  expmulzap  9989  expubnd  10000  subsq  10049  bcm1k  10156  bcpasc  10162  crim  10280  rereb  10285  fsumparts  10851  isumshft  10871  geosergap  10887  efsub  10958  sincossq  11026  efieq1re  11048  bezoutlema  11253  bezoutlemb  11254  eucialg  11306  phiprmpw  11463