Theorem 3eqtrrd 2234

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  nnanq0  7527  1idprl  7659  1idpru  7660  axcnre  7950  fseq1p1m1  10171  seqf1oglem1  10613  expmulzap  10679  expubnd  10690  subsq  10740  bcm1k  10854  bcpasc  10860  crim  11025  rereb  11030  fsumparts  11637  isumshft  11657  geosergap  11673  efsub  11848  sincossq  11915  efieq1re  11939  bezoutlema  12176  bezoutlemb  12177  eucalg  12237  phiprmpw  12400  modprmn0modprm0  12435  coprimeprodsq  12436  pythagtriplem15  12457  pythagtriplem17  12459  fldivp1  12527  1arithlem4  12545  strsetsid  12721  setsslid  12739  opprunitd  13676  cnfldsub  14141  upxp  14518  uptx  14520  perfectlem2  15246  lgsdilem  15278  gausslemma2dlem1a  15309  2sqlem3  15368