Theorem 3eqtr4a 2248

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

Syntax hints:   -> wi 4   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182

This theorem is referenced by:  uniintsnr  3895  fndmdifcom  5638  offres  6154  1stval2  6174  2ndval2  6175  ecovcom  6660  ecovass  6662  ecovdi  6664  nnnninfeq2  7145  zeo  9376  xnegneg  9851  xaddcom  9879  xaddid1  9880  xnegdi  9886  fzsuc2  10097  expnegap0  10546  facp1  10728  bcpasc  10764  hashfzp1  10822  resunimafz0  10829  absexp  11106  iooinsup  11303  fsumf1o  11416  fsumadd  11432  fisumrev2  11472  fsumparts  11496  fprodf1o  11614  fprodmul  11617  efexp  11708  tanval2ap  11739  gcdcom  11992  gcd0id  11998  dfgcd3  12029  gcdass  12034  lcmcom  12082  lcmneg  12092  lcmass  12103  sqrt2irrlem  12179  nn0gcdsq  12218  dfphi2  12238  eulerthlemth  12250  pcneg  12342  setscom  12520  restco  14071  txtopon  14159  dvef  14585  lgsneg  14822  lgsneg1  14823  lgsdir2  14831  lgsdir  14833  lgsdi  14835