Theorem 3eqtrrd 2178

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

Syntax hints:   -> wi 4   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  nnanq0  7290  1idprl  7422  1idpru  7423  axcnre  7713  fseq1p1m1  9905  expmulzap  10370  expubnd  10381  subsq  10430  bcm1k  10538  bcpasc  10544  crim  10662  rereb  10667  fsumparts  11271  isumshft  11291  geosergap  11307  efsub  11424  sincossq  11491  efieq1re  11514  bezoutlema  11723  bezoutlemb  11724  eucalg  11776  phiprmpw  11934  strsetsid  12031  setsslid  12048  upxp  12480  uptx  12482