Theorem addcli 10981

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

Syntax hints:   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869   + caddc 10874

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

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

This theorem is referenced by:  eqneg  11695  2cn  12048  3cn  12054  4cn  12058  5cn  12061  6cn  12064  7cn  12067  8cn  12070  9cn  12073  nummac  12482  binom2i  13928  sqeqori  13930  crreczi  13943  nn0opthlem1  13982  nn0opth2i  13985  3dvds2dec  16042  mod2xnegi  16772  karatsuba  16785  pige3ALT  25676  eff1o  25705  1cubrlem  25991  1cubr  25992  bposlem8  26439  ax5seglem7  27303  ipidsq  29072  ip1ilem  29188  pythi  29212  normlem2  29473  normlem3  29474  normlem7  29478  normlem9  29480  bcseqi  29482  norm-ii-i  29499  normpythi  29504  normpari  29516  polid2i  29519  lnopunilem1  30372  lnophmlem2  30379  dpmul100  31171  dpadd3  31186  dpmul4  31188  ballotlem2  32455  hgt750lem2  32632  quad3  33628  faclimlem1  33709  itg2addnclem3  35830  sqmid3api  40311  235t711  40319  sn-0tie0  40421  fltnltalem  40499  areaquad  41047  resqrtvalex  41253  imsqrtvalex  41254  fourierswlem  43771  fouriersw  43772  2t6m3t4e0  45684