Theorem addcli 10912

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

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   + caddc 10805

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

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

This theorem is referenced by:  eqneg  11625  2cn  11978  3cn  11984  4cn  11988  5cn  11991  6cn  11994  7cn  11997  8cn  12000  9cn  12003  nummac  12411  binom2i  13856  sqeqori  13858  crreczi  13871  nn0opthlem1  13910  nn0opth2i  13913  3dvds2dec  15970  mod2xnegi  16700  karatsuba  16713  pige3ALT  25581  eff1o  25610  1cubrlem  25896  1cubr  25897  bposlem8  26344  ax5seglem7  27206  ipidsq  28973  ip1ilem  29089  pythi  29113  normlem2  29374  normlem3  29375  normlem7  29379  normlem9  29381  bcseqi  29383  norm-ii-i  29400  normpythi  29405  normpari  29417  polid2i  29420  lnopunilem1  30273  lnophmlem2  30280  dpmul100  31073  dpadd3  31088  dpmul4  31090  ballotlem2  32355  hgt750lem2  32532  quad3  33528  faclimlem1  33615  itg2addnclem3  35757  sqmid3api  40232  235t711  40240  sn-0tie0  40342  fltnltalem  40415  areaquad  40963  resqrtvalex  41142  imsqrtvalex  41143  fourierswlem  43661  fouriersw  43662  2t6m3t4e0  45572