Theorem addcli 11151

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   + caddc 11041

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  eqneg  11875  2cn  12256  3cn  12262  4cn  12266  5cn  12269  6cn  12272  7cn  12275  8cn  12278  9cn  12281  nummac  12689  binom2i  14174  sqeqori  14176  crreczi  14190  nn0opthlem1  14230  nn0opth2i  14233  3dvds2dec  16302  mod2xnegi  17042  karatsuba  17054  pige3ALT  26484  eff1o  26513  1cubrlem  26805  1cubr  26806  bposlem8  27254  ax5seglem7  29004  ipidsq  30781  ip1ilem  30897  pythi  30921  normlem2  31182  normlem3  31183  normlem7  31187  normlem9  31189  bcseqi  31191  norm-ii-i  31208  normpythi  31213  normpari  31225  polid2i  31228  lnopunilem1  32081  lnophmlem2  32088  dpmul100  32956  dpadd3  32971  dpmul4  32973  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  ballotlem2  34633  hgt750lem2  34796  quad3  35852  faclimlem1  35925  itg2addnclem3  37994  sqmid3api  42715  235t711  42737  sn-0tie0  42896  fltnltalem  43095  areaquad  43644  resqrtvalex  44072  imsqrtvalex  44073  fourierswlem  46658  fouriersw  46659  2t6m3t4e0  48824