Theorem 3eqtr4a 2199

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 2189	. 2 |- ( ph -> C = B )
4		3eqtr4a.3	. 2 |- ( ph -> D = B )
5	3, 4	eqtr4d 2176	1 |- ( ph -> C = D )

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:  uniintsnr  3815  fndmdifcom  5534  offres  6041  1stval2  6061  2ndval2  6062  ecovcom  6544  ecovass  6546  ecovdi  6548  zeo  9180  xnegneg  9646  xaddcom  9674  xaddid1  9675  xnegdi  9681  fzsuc2  9890  expnegap0  10332  facp1  10508  bcpasc  10544  hashfzp1  10602  resunimafz0  10606  absexp  10883  iooinsup  11078  fsumf1o  11191  fsumadd  11207  fisumrev2  11247  fsumparts  11271  efexp  11425  tanval2ap  11456  gcdcom  11698  gcd0id  11703  dfgcd3  11734  gcdass  11739  lcmcom  11781  lcmneg  11791  lcmass  11802  sqrt2irrlem  11875  nn0gcdsq  11914  dfphi2  11932  setscom  12038  restco  12382  txtopon  12470  dvef  12896