Theorem 3eqtrrd 2269

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

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

This theorem is referenced by:  nnanq0  7738  1idprl  7870  1idpru  7871  axcnre  8161  fseq1p1m1  10391  seqf1oglem1  10844  expmulzap  10910  expubnd  10921  subsq  10971  bcm1k  11085  bcpasc  11091  crim  11498  rereb  11503  fsumparts  12111  isumshft  12131  geosergap  12147  efsub  12322  sincossq  12389  efieq1re  12413  bezoutlema  12650  bezoutlemb  12651  eucalg  12711  phiprmpw  12874  modprmn0modprm0  12909  coprimeprodsq  12910  pythagtriplem15  12931  pythagtriplem17  12933  fldivp1  13001  1arithlem4  13019  strsetsid  13195  setsslid  13213  pwsbas  13455  opprunitd  14205  cnfldsub  14671  upxp  15083  uptx  15085  perfectlem2  15814  lgsdilem  15846  gausslemma2dlem1a  15877  2sqlem3  15936