Theorem 3eqtr4a 2196

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 2186	. 2 |- ( ph -> C = B )
4		3eqtr4a.3	. 2 |- ( ph -> D = B )
5	3, 4	eqtr4d 2173	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 2119

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

This theorem is referenced by:  uniintsnr  3802  fndmdifcom  5519  offres  6026  1stval2  6046  2ndval2  6047  ecovcom  6529  ecovass  6531  ecovdi  6533  zeo  9149  xnegneg  9609  xaddcom  9637  xaddid1  9638  xnegdi  9644  fzsuc2  9852  expnegap0  10294  facp1  10469  bcpasc  10505  hashfzp1  10563  resunimafz0  10567  absexp  10844  iooinsup  11039  fsumf1o  11152  fsumadd  11168  fisumrev2  11208  fsumparts  11232  efexp  11377  tanval2ap  11409  gcdcom  11651  gcd0id  11656  dfgcd3  11687  gcdass  11692  lcmcom  11734  lcmneg  11744  lcmass  11755  sqrt2irrlem  11828  nn0gcdsq  11867  dfphi2  11885  setscom  11988  restco  12332  txtopon  12420  dvef  12845