Theorem addcli 11210

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

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   + caddc 11098

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  eqneg  11930  2cn  12311  3cn  12317  4cn  12321  5cn  12324  6cn  12327  7cn  12330  8cn  12333  9cn  12336  nummac  12756  binom2i  14244  sqeqori  14246  crreczi  14260  nn0opthlem1  14300  nn0opth2i  14303  3dvds2dec  16386  mod2xnegi  17126  karatsuba  17138  pige3ALT  26685  eff1o  26714  1cubrlem  27006  1cubr  27007  bposlem8  27455  ax5seglem7  29285  ipidsq  31062  ip1ilem  31178  pythi  31202  normlem2  31463  normlem3  31464  normlem7  31468  normlem9  31470  bcseqi  31472  norm-ii-i  31489  normpythi  31494  normpari  31506  polid2i  31509  lnopunilem1  32362  lnophmlem2  32369  dpmul100  33216  dpadd3  33231  dpmul4  33233  cos9thpiminplylem4  34175  cos9thpiminplylem5  34176  ballotlem2  34879  hgt750lem2  35039  quad3  36162  faclimlem1  36235  itg2addnclem3  38344  25or6to4  42993  sqmid3api  43064  235t711  43086  sn-0tie0  43245  fltnltalem  43414  areaquad  43963  resqrtvalex  44391  imsqrtvalex  44392  fourierswlem  46964  fouriersw  46965  2t6m3t4e0  49148  crossp3i  50668