Theorem 3eqtr4a 2198

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

Syntax hints:   -> wi 4   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  uniintsnr  3807  fndmdifcom  5526  offres  6033  1stval2  6053  2ndval2  6054  ecovcom  6536  ecovass  6538  ecovdi  6540  zeo  9156  xnegneg  9616  xaddcom  9644  xaddid1  9645  xnegdi  9651  fzsuc2  9859  expnegap0  10301  facp1  10476  bcpasc  10512  hashfzp1  10570  resunimafz0  10574  absexp  10851  iooinsup  11046  fsumf1o  11159  fsumadd  11175  fisumrev2  11215  fsumparts  11239  efexp  11388  tanval2ap  11420  gcdcom  11662  gcd0id  11667  dfgcd3  11698  gcdass  11703  lcmcom  11745  lcmneg  11755  lcmass  11766  sqrt2irrlem  11839  nn0gcdsq  11878  dfphi2  11896  setscom  11999  restco  12343  txtopon  12431  dvef  12856