Theorem 3eqtrrd 2226

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

Syntax hints:   -> wi 4   = wceq 1363

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2170

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

This theorem is referenced by:  nnanq0  7474  1idprl  7606  1idpru  7607  axcnre  7897  fseq1p1m1  10111  expmulzap  10583  expubnd  10594  subsq  10644  bcm1k  10757  bcpasc  10763  crim  10884  rereb  10889  fsumparts  11495  isumshft  11515  geosergap  11531  efsub  11706  sincossq  11773  efieq1re  11796  bezoutlema  12017  bezoutlemb  12018  eucalg  12076  phiprmpw  12239  modprmn0modprm0  12273  coprimeprodsq  12274  pythagtriplem15  12295  pythagtriplem17  12297  fldivp1  12363  1arithlem4  12381  strsetsid  12512  setsslid  12530  opprunitd  13420  cnfldsub  13838  upxp  14155  uptx  14157  lgsdilem  14811  2sqlem3  14847