Theorem 3eqtrrd 2268

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2212

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

This theorem is referenced by:  nnanq0  7683  1idprl  7815  1idpru  7816  axcnre  8106  fseq1p1m1  10334  seqf1oglem1  10787  expmulzap  10853  expubnd  10864  subsq  10914  bcm1k  11028  bcpasc  11034  crim  11441  rereb  11446  fsumparts  12054  isumshft  12074  geosergap  12090  efsub  12265  sincossq  12332  efieq1re  12356  bezoutlema  12593  bezoutlemb  12594  eucalg  12654  phiprmpw  12817  modprmn0modprm0  12852  coprimeprodsq  12853  pythagtriplem15  12874  pythagtriplem17  12876  fldivp1  12944  1arithlem4  12962  strsetsid  13138  setsslid  13156  pwsbas  13398  opprunitd  14148  cnfldsub  14613  upxp  15025  uptx  15027  perfectlem2  15753  lgsdilem  15785  gausslemma2dlem1a  15816  2sqlem3  15875