Theorem addcli 11250

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

Syntax hints:   ∈ wcel 2098  (class class class)co 7417  ℂcc 11136   + caddc 11141

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

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

This theorem is referenced by:  eqneg  11964  2cn  12317  3cn  12323  4cn  12327  5cn  12330  6cn  12333  7cn  12336  8cn  12339  9cn  12342  nummac  12752  binom2i  14207  sqeqori  14209  crreczi  14222  nn0opthlem1  14259  nn0opth2i  14262  3dvds2dec  16309  mod2xnegi  17039  karatsuba  17052  pige3ALT  26484  eff1o  26513  1cubrlem  26803  1cubr  26804  bposlem8  27254  ax5seglem7  28802  ipidsq  30576  ip1ilem  30692  pythi  30716  normlem2  30977  normlem3  30978  normlem7  30982  normlem9  30984  bcseqi  30986  norm-ii-i  31003  normpythi  31008  normpari  31020  polid2i  31023  lnopunilem1  31876  lnophmlem2  31883  dpmul100  32677  dpadd3  32692  dpmul4  32694  ballotlem2  34178  hgt750lem2  34354  quad3  35344  faclimlem1  35407  itg2addnclem3  37216  sqmid3api  41922  235t711  41932  sn-0tie0  42059  fltnltalem  42151  areaquad  42709  resqrtvalex  43140  imsqrtvalex  43141  fourierswlem  45681  fouriersw  45682  2t6m3t4e0  47524