Theorem addcli 11150

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 7368  ℂ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  11873  2cn  12232  3cn  12238  4cn  12242  5cn  12245  6cn  12248  7cn  12251  8cn  12254  9cn  12257  nummac  12664  binom2i  14147  sqeqori  14149  crreczi  14163  nn0opthlem1  14203  nn0opth2i  14206  3dvds2dec  16272  mod2xnegi  17011  karatsuba  17023  pige3ALT  26500  eff1o  26529  1cubrlem  26822  1cubr  26823  bposlem8  27273  ax5seglem7  29024  ipidsq  30802  ip1ilem  30918  pythi  30942  normlem2  31203  normlem3  31204  normlem7  31208  normlem9  31210  bcseqi  31212  norm-ii-i  31229  normpythi  31234  normpari  31246  polid2i  31249  lnopunilem1  32102  lnophmlem2  32109  dpmul100  32993  dpadd3  33008  dpmul4  33010  cos9thpiminplylem4  33967  cos9thpiminplylem5  33968  ballotlem2  34671  hgt750lem2  34834  quad3  35890  faclimlem1  35963  itg2addnclem3  37928  sqmid3api  42657  235t711  42679  sn-0tie0  42825  fltnltalem  43024  areaquad  43577  resqrtvalex  44005  imsqrtvalex  44006  fourierswlem  46592  fouriersw  46593  2t6m3t4e0  48712