Theorem 3eqtrrd 2215

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  nnanq0  7457  1idprl  7589  1idpru  7590  axcnre  7880  fseq1p1m1  10094  expmulzap  10566  expubnd  10577  subsq  10627  bcm1k  10740  bcpasc  10746  crim  10867  rereb  10872  fsumparts  11478  isumshft  11498  geosergap  11514  efsub  11689  sincossq  11756  efieq1re  11779  bezoutlema  12000  bezoutlemb  12001  eucalg  12059  phiprmpw  12222  modprmn0modprm0  12256  coprimeprodsq  12257  pythagtriplem15  12278  pythagtriplem17  12280  fldivp1  12346  1arithlem4  12364  strsetsid  12495  setsslid  12513  opprunitd  13279  cnfldsub  13472  upxp  13775  uptx  13777  lgsdilem  14431  2sqlem3  14467