Theorem addcli 11217

Description: Closure law for addition. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ

Assertion

Ref	Expression
addcli	⊢ (𝐴 + 𝐵) ∈ ℂ

Proof of Theorem addcli

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		addcl 11189	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 691	1 ⊢ (𝐴 + 𝐵) ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105   + caddc 11110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 11167

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  eqneg  11931  2cn  12284  3cn  12290  4cn  12294  5cn  12297  6cn  12300  7cn  12303  8cn  12306  9cn  12309  nummac  12719  binom2i  14173  sqeqori  14175  crreczi  14188  nn0opthlem1  14225  nn0opth2i  14228  3dvds2dec  16273  mod2xnegi  17001  karatsuba  17014  pige3ALT  26021  eff1o  26050  1cubrlem  26336  1cubr  26337  bposlem8  26784  ax5seglem7  28183  ipidsq  29951  ip1ilem  30067  pythi  30091  normlem2  30352  normlem3  30353  normlem7  30357  normlem9  30359  bcseqi  30361  norm-ii-i  30378  normpythi  30383  normpari  30395  polid2i  30398  lnopunilem1  31251  lnophmlem2  31258  dpmul100  32051  dpadd3  32066  dpmul4  32068  ballotlem2  33476  hgt750lem2  33653  quad3  34644  faclimlem1  34702  itg2addnclem3  36530  sqmid3api  41193  235t711  41201  sn-0tie0  41309  fltnltalem  41401  areaquad  41951  resqrtvalex  42382  imsqrtvalex  42383  fourierswlem  44933  fouriersw  44934  2t6m3t4e0  46978