Theorem 3eqtrrd 2276

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  nnanq0  7825  1idprl  7957  1idpru  7958  axcnre  8248  fseq1p1m1  10501  seqf1oglem1  10956  expmulzap  11022  expubnd  11033  subsq  11083  bcm1k  11198  bcpasc  11204  crim  11623  rereb  11628  fsumparts  12237  isumshft  12257  geosergap  12273  efsub  12448  sincossq  12515  efieq1re  12539  bezoutlema  12776  bezoutlemb  12777  eucalg  12837  phiprmpw  13000  modprmn0modprm0  13035  coprimeprodsq  13036  pythagtriplem15  13057  pythagtriplem17  13059  fldivp1  13127  1arithlem4  13145  ballotfilemi1  13245  ballotfilemii  13246  ballotfilemic  13250  ballotfilem1c  13251  strsetsid  13385  setsslid  13403  pwsbas  14205  opprunitd  14417  cnfldsub  14912  upxp  15373  uptx  15375  perfectlem2  16114  lgsdilem  16146  gausslemma2dlem1a  16177  2sqlem3  16236