Theorem 3eqtr4a 2297

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  uniintsnr  4006  fndmdifcom  5818  funopsn  5894  offres  6372  1stval2  6393  2ndval2  6394  ecovcom  6921  ecovass  6923  ecovdi  6925  nnnninfeq2  7475  zeo  9761  xnegneg  10251  xaddcom  10279  xaddid1  10280  xnegdi  10286  fzsuc2  10502  expnegap0  11004  resq01  11115  facp1  11189  bcpasc  11225  hashfzp1  11286  resunimafz0  11295  hashfibclem  11303  hashfibc  11304  hashf1  11308  ccat1st1st  11430  sq01  11681  absexp  11867  iooinsup  12067  fsumf1o  12181  fsumadd  12197  fisumrev2  12237  fsumparts  12261  fprodf1o  12379  fprodmul  12382  efexp  12473  tanval2ap  12504  gcdcom  12774  gcd0id  12780  dfgcd3  12811  gcdass  12816  lcmcom  12866  lcmneg  12876  lcmass  12887  sqrt2irrlem  12964  nn0gcdsq  13004  dfphi2  13026  eulerthlemth  13038  pcneg  13132  setscom  13449  gsum2dfilem2  14271  gsumcom2fi  14274  restco  15417  txtopon  15505  dvmptid  15959  dvef  15970  logfac  16143  log2tlbndlog2  16237  fsumdvdsmul  16302  bcp1ctr  16323  lgsneg  16365  lgsneg1  16366  lgsdir2  16374  lgsdir  16376  lgsdi  16378  lgsquad2lem2  16423  egrsubgr  16726