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	⊢ 𝐴 = 𝐵
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 2278	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2265	1 ⊢ (𝜑 → 𝐶 = 𝐷)

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  11187  absexp  11605  iooinsup  11803  fsumf1o  11916  fsumadd  11932  fisumrev2  11972  fsumparts  11996  fprodf1o  12114  fprodmul  12117  efexp  12208  tanval2ap  12239  gcdcom  12509  gcd0id  12515  dfgcd3  12546  gcdass  12551  lcmcom  12601  lcmneg  12611  lcmass  12622  sqrt2irrlem  12698  nn0gcdsq  12737  dfphi2  12757  eulerthlemth  12769  pcneg  12863  setscom  13087  gsumfzfsumlem0  14565  restco  14863  txtopon  14951  dvmptid  15405  dvef  15416  fsumdvdsmul  15680  lgsneg  15718  lgsneg1  15719  lgsdir2  15727  lgsdir  15729  lgsdi  15731  lgsquad2lem2  15776