Theorem addcli 11146

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

Syntax hints:   ∈ wcel 2121  (class class class)co 7360  ℂcc 11031   + caddc 11036

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

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

This theorem is referenced by:  eqneg  11870  2cn  12251  3cn  12257  4cn  12261  5cn  12264  6cn  12267  7cn  12270  8cn  12273  9cn  12276  nummac  12684  binom2i  14169  sqeqori  14171  crreczi  14185  nn0opthlem1  14225  nn0opth2i  14228  3dvds2dec  16297  mod2xnegi  17037  karatsuba  17049  pige3ALT  26506  eff1o  26535  1cubrlem  26827  1cubr  26828  bposlem8  27276  ax5seglem7  29026  ipidsq  30803  ip1ilem  30919  pythi  30943  normlem2  31204  normlem3  31205  normlem7  31209  normlem9  31211  bcseqi  31213  norm-ii-i  31230  normpythi  31235  normpari  31247  polid2i  31250  lnopunilem1  32103  lnophmlem2  32110  dpmul100  32979  dpadd3  32994  dpmul4  32996  cos9thpiminplylem4  33981  cos9thpiminplylem5  33982  ballotlem2  34685  hgt750lem2  34848  quad3  35913  faclimlem1  35986  itg2addnclem3  38055  sqmid3api  42775  235t711  42797  sn-0tie0  42956  fltnltalem  43127  areaquad  43676  resqrtvalex  44104  imsqrtvalex  44105  fourierswlem  46687  fouriersw  46688  2t6m3t4e0  48853