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  7645  1idprl  7777  1idpru  7778  axcnre  8068  fseq1p1m1  10290  seqf1oglem1  10741  expmulzap  10807  expubnd  10818  subsq  10868  bcm1k  10982  bcpasc  10988  crim  11369  rereb  11374  fsumparts  11981  isumshft  12001  geosergap  12017  efsub  12192  sincossq  12259  efieq1re  12283  bezoutlema  12520  bezoutlemb  12521  eucalg  12581  phiprmpw  12744  modprmn0modprm0  12779  coprimeprodsq  12780  pythagtriplem15  12801  pythagtriplem17  12803  fldivp1  12871  1arithlem4  12889  strsetsid  13065  setsslid  13083  pwsbas  13325  opprunitd  14074  cnfldsub  14539  upxp  14946  uptx  14948  perfectlem2  15674  lgsdilem  15706  gausslemma2dlem1a  15737  2sqlem3  15796