Theorem 3eqtr4a 2288

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  uniintsnr  3959  fndmdifcom  5743  funopsn  5819  offres  6286  1stval2  6307  2ndval2  6308  ecovcom  6797  ecovass  6799  ecovdi  6801  nnnninfeq2  7307  zeo  9563  xnegneg  10041  xaddcom  10069  xaddid1  10070  xnegdi  10076  fzsuc2  10287  expnegap0  10781  facp1  10964  bcpasc  11000  hashfzp1  11059  resunimafz0  11066  ccat1st1st  11188  absexp  11606  iooinsup  11804  fsumf1o  11917  fsumadd  11933  fisumrev2  11973  fsumparts  11997  fprodf1o  12115  fprodmul  12118  efexp  12209  tanval2ap  12240  gcdcom  12510  gcd0id  12516  dfgcd3  12547  gcdass  12552  lcmcom  12602  lcmneg  12612  lcmass  12623  sqrt2irrlem  12699  nn0gcdsq  12738  dfphi2  12758  eulerthlemth  12770  pcneg  12864  setscom  13088  gsumfzfsumlem0  14566  restco  14864  txtopon  14952  dvmptid  15406  dvef  15417  fsumdvdsmul  15681  lgsneg  15719  lgsneg1  15720  lgsdir2  15728  lgsdir  15730  lgsdi  15732  lgsquad2lem2  15777