Theorem 3eqtr4a 2290

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  uniintsnr  3964  fndmdifcom  5753  funopsn  5829  offres  6296  1stval2  6317  2ndval2  6318  ecovcom  6810  ecovass  6812  ecovdi  6814  nnnninfeq2  7327  zeo  9584  xnegneg  10067  xaddcom  10095  xaddid1  10096  xnegdi  10102  fzsuc2  10313  expnegap0  10808  facp1  10991  bcpasc  11027  hashfzp1  11087  resunimafz0  11094  ccat1st1st  11217  absexp  11639  iooinsup  11837  fsumf1o  11950  fsumadd  11966  fisumrev2  12006  fsumparts  12030  fprodf1o  12148  fprodmul  12151  efexp  12242  tanval2ap  12273  gcdcom  12543  gcd0id  12549  dfgcd3  12580  gcdass  12585  lcmcom  12635  lcmneg  12645  lcmass  12656  sqrt2irrlem  12732  nn0gcdsq  12771  dfphi2  12791  eulerthlemth  12803  pcneg  12897  setscom  13121  gsumfzfsumlem0  14599  restco  14897  txtopon  14985  dvmptid  15439  dvef  15450  fsumdvdsmul  15714  lgsneg  15752  lgsneg1  15753  lgsdir2  15761  lgsdir  15763  lgsdi  15765  lgsquad2lem2  15810  egrsubgr  16113