Theorem addcli 11215

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

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℂcc 11098   + caddc 11103

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  eqneg  11935  2cn  12316  3cn  12322  4cn  12326  5cn  12329  6cn  12332  7cn  12335  8cn  12338  9cn  12341  nummac  12761  binom2i  14248  sqeqori  14250  crreczi  14264  nn0opthlem1  14304  nn0opth2i  14307  3dvds2dec  16391  mod2xnegi  17131  karatsuba  17143  pige3ALT  26651  eff1o  26680  1cubrlem  26972  1cubr  26973  bposlem8  27421  ax5seglem7  29226  ipidsq  31003  ip1ilem  31119  pythi  31143  normlem2  31404  normlem3  31405  normlem7  31409  normlem9  31411  bcseqi  31413  norm-ii-i  31430  normpythi  31435  normpari  31447  polid2i  31450  lnopunilem1  32303  lnophmlem2  32310  dpmul100  33157  dpadd3  33172  dpmul4  33174  cos9thpiminplylem4  34120  cos9thpiminplylem5  34121  ballotlem2  34824  hgt750lem2  34984  quad3  36095  faclimlem1  36168  itg2addnclem3  38246  25or6to4  42897  sqmid3api  42968  235t711  42990  sn-0tie0  43149  fltnltalem  43320  areaquad  43869  resqrtvalex  44297  imsqrtvalex  44298  fourierswlem  46870  fouriersw  46871  2t6m3t4e0  49047