Theorem addcli 11136

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

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022   + caddc 11027

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

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

This theorem is referenced by:  eqneg  11859  2cn  12218  3cn  12224  4cn  12228  5cn  12231  6cn  12234  7cn  12237  8cn  12240  9cn  12243  nummac  12650  binom2i  14133  sqeqori  14135  crreczi  14149  nn0opthlem1  14189  nn0opth2i  14192  3dvds2dec  16258  mod2xnegi  16997  karatsuba  17009  pige3ALT  26483  eff1o  26512  1cubrlem  26805  1cubr  26806  bposlem8  27256  ax5seglem7  28957  ipidsq  30734  ip1ilem  30850  pythi  30874  normlem2  31135  normlem3  31136  normlem7  31140  normlem9  31142  bcseqi  31144  norm-ii-i  31161  normpythi  31166  normpari  31178  polid2i  31181  lnopunilem1  32034  lnophmlem2  32041  dpmul100  32927  dpadd3  32942  dpmul4  32944  cos9thpiminplylem4  33891  cos9thpiminplylem5  33892  ballotlem2  34595  hgt750lem2  34758  quad3  35813  faclimlem1  35886  itg2addnclem3  37813  sqmid3api  42480  235t711  42502  sn-0tie0  42648  fltnltalem  42847  areaquad  43400  resqrtvalex  43828  imsqrtvalex  43829  fourierswlem  46416  fouriersw  46417  2t6m3t4e0  48536