Theorem addcli 11143

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

Syntax hints:   ∈ wcel 2119  (class class class)co 7357  ℂcc 11028   + caddc 11033

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

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  eqneg  11867  2cn  12248  3cn  12254  4cn  12258  5cn  12261  6cn  12264  7cn  12267  8cn  12270  9cn  12273  nummac  12681  binom2i  14166  sqeqori  14168  crreczi  14182  nn0opthlem1  14222  nn0opth2i  14225  3dvds2dec  16294  mod2xnegi  17034  karatsuba  17046  pige3ALT  26503  eff1o  26532  1cubrlem  26824  1cubr  26825  bposlem8  27273  ax5seglem7  29023  ipidsq  30800  ip1ilem  30916  pythi  30940  normlem2  31201  normlem3  31202  normlem7  31206  normlem9  31208  bcseqi  31210  norm-ii-i  31227  normpythi  31232  normpari  31244  polid2i  31247  lnopunilem1  32100  lnophmlem2  32107  dpmul100  32976  dpadd3  32991  dpmul4  32993  cos9thpiminplylem4  33978  cos9thpiminplylem5  33979  ballotlem2  34682  hgt750lem2  34845  quad3  35907  faclimlem1  35980  itg2addnclem3  38049  sqmid3api  42769  235t711  42791  sn-0tie0  42950  fltnltalem  43121  areaquad  43670  resqrtvalex  44098  imsqrtvalex  44099  fourierswlem  46681  fouriersw  46682  2t6m3t4e0  48847