Theorem 3eqtrrd 2243

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

Syntax hints:   -> wi 4   = wceq 1373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198

This theorem is referenced by:  nnanq0  7573  1idprl  7705  1idpru  7706  axcnre  7996  fseq1p1m1  10218  seqf1oglem1  10666  expmulzap  10732  expubnd  10743  subsq  10793  bcm1k  10907  bcpasc  10913  crim  11202  rereb  11207  fsumparts  11814  isumshft  11834  geosergap  11850  efsub  12025  sincossq  12092  efieq1re  12116  bezoutlema  12353  bezoutlemb  12354  eucalg  12414  phiprmpw  12577  modprmn0modprm0  12612  coprimeprodsq  12613  pythagtriplem15  12634  pythagtriplem17  12636  fldivp1  12704  1arithlem4  12722  strsetsid  12898  setsslid  12916  pwsbas  13157  opprunitd  13905  cnfldsub  14370  upxp  14777  uptx  14779  perfectlem2  15505  lgsdilem  15537  gausslemma2dlem1a  15568  2sqlem3  15627