Theorem 3eqtrrd 2270

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  nnanq0  7773  1idprl  7905  1idpru  7906  axcnre  8196  fseq1p1m1  10428  seqf1oglem1  10881  expmulzap  10947  expubnd  10958  subsq  11008  bcm1k  11122  bcpasc  11128  crim  11543  rereb  11548  fsumparts  12156  isumshft  12176  geosergap  12192  efsub  12367  sincossq  12434  efieq1re  12458  bezoutlema  12695  bezoutlemb  12696  eucalg  12756  phiprmpw  12919  modprmn0modprm0  12954  coprimeprodsq  12955  pythagtriplem15  12976  pythagtriplem17  12978  fldivp1  13046  1arithlem4  13064  strsetsid  13245  setsslid  13263  pwsbas  13505  opprunitd  14255  cnfldsub  14723  upxp  15137  uptx  15139  perfectlem2  15868  lgsdilem  15900  gausslemma2dlem1a  15931  2sqlem3  15990