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  5815  funopsn  5891  offres  6368  1stval2  6389  2ndval2  6390  ecovcom  6916  ecovass  6918  ecovdi  6920  nnnninfeq2  7469  zeo  9755  xnegneg  10245  xaddcom  10273  xaddid1  10274  xnegdi  10280  fzsuc2  10496  expnegap0  10997  resq01  11108  facp1  11182  bcpasc  11218  hashfzp1  11279  resunimafz0  11288  hashfibclem  11296  hashfibc  11297  hashf1  11301  ccat1st1st  11423  sq01  11674  absexp  11860  iooinsup  12059  fsumf1o  12173  fsumadd  12189  fisumrev2  12229  fsumparts  12253  fprodf1o  12371  fprodmul  12374  efexp  12465  tanval2ap  12496  gcdcom  12766  gcd0id  12772  dfgcd3  12803  gcdass  12808  lcmcom  12858  lcmneg  12868  lcmass  12879  sqrt2irrlem  12956  nn0gcdsq  12996  dfphi2  13018  eulerthlemth  13030  pcneg  13124  setscom  13441  restco  15324  txtopon  15412  dvmptid  15866  dvef  15877  logfac  16048  log2tlbndlog2  16139  fsumdvdsmul  16186  bcp1ctr  16204  lgsneg  16241  lgsneg1  16242  lgsdir2  16250  lgsdir  16252  lgsdi  16254  lgsquad2lem2  16299  egrsubgr  16602