Theorem addcli 10647

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   + caddc 10540

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

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

This theorem is referenced by:  eqneg  11360  2cn  11713  3cn  11719  4cn  11723  5cn  11726  6cn  11729  7cn  11732  8cn  11735  9cn  11738  nummac  12144  binom2i  13575  sqeqori  13577  crreczi  13590  nn0opthlem1  13629  nn0opth2i  13632  3dvds2dec  15682  mod2xnegi  16407  karatsuba  16420  pige3ALT  25105  eff1o  25133  1cubrlem  25419  1cubr  25420  bposlem8  25867  ax5seglem7  26721  ipidsq  28487  ip1ilem  28603  pythi  28627  normlem2  28888  normlem3  28889  normlem7  28893  normlem9  28895  bcseqi  28897  norm-ii-i  28914  normpythi  28919  normpari  28931  polid2i  28934  lnopunilem1  29787  lnophmlem2  29794  dpmul100  30573  dpadd3  30588  dpmul4  30590  ballotlem2  31746  hgt750lem2  31923  quad3  32913  faclimlem1  32975  itg2addnclem3  34960  sqmid3api  39189  235t711  39197  fltnltalem  39294  areaquad  39843  fourierswlem  42535  fouriersw  42536  2t6m3t4e0  44416