Theorem 3eqtrrd 2208

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

Syntax hints:   -> wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  nnanq0  7413  1idprl  7545  1idpru  7546  axcnre  7836  fseq1p1m1  10043  expmulzap  10515  expubnd  10526  subsq  10575  bcm1k  10687  bcpasc  10693  crim  10815  rereb  10820  fsumparts  11426  isumshft  11446  geosergap  11462  efsub  11637  sincossq  11704  efieq1re  11727  bezoutlema  11947  bezoutlemb  11948  eucalg  12006  phiprmpw  12169  modprmn0modprm0  12203  coprimeprodsq  12204  pythagtriplem15  12225  pythagtriplem17  12227  fldivp1  12293  1arithlem4  12311  strsetsid  12442  setsslid  12459  upxp  13031  uptx  13033  lgsdilem  13687  2sqlem3  13712