Theorem 3eqtr4a 2264

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  uniintsnr  3921  fndmdifcom  5688  funopsn  5764  offres  6222  1stval2  6243  2ndval2  6244  ecovcom  6731  ecovass  6733  ecovdi  6735  nnnninfeq2  7233  zeo  9480  xnegneg  9957  xaddcom  9985  xaddid1  9986  xnegdi  9992  fzsuc2  10203  expnegap0  10694  facp1  10877  bcpasc  10913  hashfzp1  10971  resunimafz0  10978  ccat1st1st  11096  absexp  11423  iooinsup  11621  fsumf1o  11734  fsumadd  11750  fisumrev2  11790  fsumparts  11814  fprodf1o  11932  fprodmul  11935  efexp  12026  tanval2ap  12057  gcdcom  12327  gcd0id  12333  dfgcd3  12364  gcdass  12369  lcmcom  12419  lcmneg  12429  lcmass  12440  sqrt2irrlem  12516  nn0gcdsq  12555  dfphi2  12575  eulerthlemth  12587  pcneg  12681  setscom  12905  gsumfzfsumlem0  14381  restco  14679  txtopon  14767  dvmptid  15221  dvef  15232  fsumdvdsmul  15496  lgsneg  15534  lgsneg1  15535  lgsdir2  15543  lgsdir  15545  lgsdi  15547  lgsquad2lem2  15592