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	⊢ 𝐴 = 𝐵
3eqtr4a.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4a.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4a	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4a

Step	Hyp	Ref	Expression
1		3eqtr4a.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eqtr4a.1	. . 3 ⊢ 𝐴 = 𝐵
3	1, 2	eqtrdi 2287	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2274	1 ⊢ (𝜑 → 𝐶 = 𝐷)

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  6920  ecovass  6922  ecovdi  6924  nnnninfeq2  7475  zeo  9762  xnegneg  10252  xaddcom  10280  xaddid1  10281  xnegdi  10287  fzsuc2  10503  expnegap0  11005  resq01  11116  facp1  11190  bcpasc  11226  hashfzp1  11287  resunimafz0  11296  hashfibclem  11304  hashfibc  11305  hashf1  11309  ccat1st1st  11431  sq01  11682  absexp  11868  iooinsup  12068  fsumf1o  12182  fsumadd  12198  fisumrev2  12238  fsumparts  12262  fprodf1o  12380  fprodmul  12383  efexp  12474  tanval2ap  12505  gcdcom  12775  gcd0id  12781  dfgcd3  12812  gcdass  12817  lcmcom  12867  lcmneg  12877  lcmass  12888  sqrt2irrlem  12965  nn0gcdsq  13005  dfphi2  13027  eulerthlemth  13039  pcneg  13133  setscom  13450  gsum2dfilem2  14272  gsumcom2fi  14275  restco  15400  txtopon  15488  dvmptid  15942  dvef  15953  logfac  16126  log2tlbndlog2  16220  fsumdvdsmul  16285  bcp1ctr  16306  lgsneg  16348  lgsneg1  16349  lgsdir2  16357  lgsdir  16359  lgsdi  16361  lgsquad2lem2  16406  egrsubgr  16709