Theorem 3eqtr4a 2224

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4a.1	|- A = B
3eqtr4a.2	|- ( ph -> C = A )
3eqtr4a.3	|- ( ph -> D = B )

Assertion

Ref	Expression
3eqtr4a	|- ( ph -> C = D )

Proof of Theorem 3eqtr4a

Step	Hyp	Ref	Expression
1		3eqtr4a.2	. . 3 |- ( ph -> C = A )
2		3eqtr4a.1	. . 3 |- A = B
3	1, 2	eqtrdi 2214	. 2 |- ( ph -> C = B )
4		3eqtr4a.3	. 2 |- ( ph -> D = B )
5	3, 4	eqtr4d 2201	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  uniintsnr  3859  fndmdifcom  5590  offres  6100  1stval2  6120  2ndval2  6121  ecovcom  6604  ecovass  6606  ecovdi  6608  nnnninfeq2  7089  zeo  9292  xnegneg  9765  xaddcom  9793  xaddid1  9794  xnegdi  9800  fzsuc2  10010  expnegap0  10459  facp1  10639  bcpasc  10675  hashfzp1  10733  resunimafz0  10740  absexp  11017  iooinsup  11214  fsumf1o  11327  fsumadd  11343  fisumrev2  11383  fsumparts  11407  fprodf1o  11525  fprodmul  11528  efexp  11619  tanval2ap  11650  gcdcom  11902  gcd0id  11908  dfgcd3  11939  gcdass  11944  lcmcom  11992  lcmneg  12002  lcmass  12013  sqrt2irrlem  12089  nn0gcdsq  12128  dfphi2  12148  eulerthlemth  12160  pcneg  12252  setscom  12430  restco  12774  txtopon  12862  dvef  13288  lgsneg  13525  lgsneg1  13526  lgsdir2  13534  lgsdir  13536  lgsdi  13538