Theorem 3eqtrrd 2267

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  nnanq0  7656  1idprl  7788  1idpru  7789  axcnre  8079  fseq1p1m1  10302  seqf1oglem1  10753  expmulzap  10819  expubnd  10830  subsq  10880  bcm1k  10994  bcpasc  11000  crim  11385  rereb  11390  fsumparts  11997  isumshft  12017  geosergap  12033  efsub  12208  sincossq  12275  efieq1re  12299  bezoutlema  12536  bezoutlemb  12537  eucalg  12597  phiprmpw  12760  modprmn0modprm0  12795  coprimeprodsq  12796  pythagtriplem15  12817  pythagtriplem17  12819  fldivp1  12887  1arithlem4  12905  strsetsid  13081  setsslid  13099  pwsbas  13341  opprunitd  14090  cnfldsub  14555  upxp  14962  uptx  14964  perfectlem2  15690  lgsdilem  15722  gausslemma2dlem1a  15753  2sqlem3  15812