Theorem 3eqtrrd 2177

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 2172	. 2 |- ( ph -> A = C )
4		3eqtrd.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtr2d 2173	1 |- ( ph -> D = A )

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  nnanq0  7266  1idprl  7398  1idpru  7399  axcnre  7689  fseq1p1m1  9874  expmulzap  10339  expubnd  10350  subsq  10399  bcm1k  10506  bcpasc  10512  crim  10630  rereb  10635  fsumparts  11239  isumshft  11259  geosergap  11275  efsub  11387  sincossq  11455  efieq1re  11478  bezoutlema  11687  bezoutlemb  11688  eucalg  11740  phiprmpw  11898  strsetsid  11992  setsslid  12009  upxp  12441  uptx  12443