Theorem addcli 10335

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 10306	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 684	1 ⊢ (𝐴 + 𝐵) ∈ ℂ

Syntax hints:   ∈ wcel 2157  (class class class)co 6878  ℂcc 10222   + caddc 10227

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

This theorem depends on definitions:  df-bi 199  df-an 386

This theorem is referenced by:  eqneg  11037  2cn  11388  3cn  11394  4cn  11399  5cn  11403  6cn  11407  7cn  11411  8cn  11415  9cn  11419  nummac  11829  binom2i  13228  sqeqori  13230  crreczi  13243  nn0opthlem1  13308  nn0opth2i  13311  3dvds2dec  15393  mod2xnegi  16108  karatsuba  16121  pige3  24611  eff1o  24637  1cubrlem  24920  1cubr  24921  bposlem8  25368  ax5seglem7  26172  ipidsq  28090  ip1ilem  28206  pythi  28230  normlem2  28493  normlem3  28494  normlem7  28498  normlem9  28500  bcseqi  28502  norm-ii-i  28519  normpythi  28524  normpari  28536  polid2i  28539  lnopunilem1  29394  lnophmlem2  29401  dpmul100  30121  dpadd3  30136  dpmul4  30138  ballotlem2  31067  hgt750lem2  31250  quad3  32079  faclimlem1  32143  itg2addnclem3  33951  sqmid3api  37994  235t711  38002  areaquad  38586  fourierswlem  41190  fouriersw  41191  2t6m3t4e0  42925