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  9751  xnegneg  10235  xaddcom  10263  xaddid1  10264  xnegdi  10270  fzsuc2  10486  expnegap0  10984  resq01  11095  facp1  11168  bcpasc  11204  hashfzp1  11265  resunimafz0  11274  hashfibclem  11282  hashfibc  11283  hashf1  11287  ccat1st1st  11409  sq01  11660  absexp  11845  iooinsup  12043  fsumf1o  12157  fsumadd  12173  fisumrev2  12213  fsumparts  12237  fprodf1o  12355  fprodmul  12358  efexp  12449  tanval2ap  12480  gcdcom  12750  gcd0id  12756  dfgcd3  12787  gcdass  12792  lcmcom  12842  lcmneg  12852  lcmass  12863  sqrt2irrlem  12939  nn0gcdsq  12978  dfphi2  12998  eulerthlemth  13010  pcneg  13104  setscom  13392  restco  15275  txtopon  15363  dvmptid  15817  dvef  15828  logfac  15995  log2tlbndlog2  16082  fsumdvdsmul  16105  lgsneg  16143  lgsneg1  16144  lgsdir2  16152  lgsdir  16154  lgsdi  16156  lgsquad2lem2  16201  egrsubgr  16504