Theorem 3eqtr4a 2140

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

Syntax hints:   -> wi 4   = wceq 1285

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075

This theorem is referenced by:  uniintsnr  3680  fndmdifcom  5305  offres  5793  1stval2  5813  2ndval2  5814  ecovcom  6279  ecovass  6281  ecovdi  6283  zeo  8533  xnegneg  8976  fzsuc2  9172  expnegap0  9581  facp1  9754  bcpasc  9790  absexp  10103  gcdcom  10509  gcd0id  10514  dfgcd3  10543  gcdass  10548  lcmcom  10590  lcmneg  10600  lcmass  10611  sqrt2irrlem  10684