Theorem addcli 10385

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

Syntax hints:   ∈ wcel 2107  (class class class)co 6924  ℂcc 10272   + caddc 10277

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

This theorem depends on definitions:  df-bi 199  df-an 387

This theorem is referenced by:  eqneg  11097  2cn  11454  3cn  11460  4cn  11465  5cn  11469  6cn  11473  7cn  11477  8cn  11481  9cn  11485  nummac  11895  binom2i  13297  sqeqori  13299  crreczi  13312  nn0opthlem1  13377  nn0opth2i  13380  3dvds2dec  15465  mod2xnegi  16183  karatsuba  16196  pige3  24711  eff1o  24737  1cubrlem  25023  1cubr  25024  bposlem8  25472  ax5seglem7  26288  ipidsq  28141  ip1ilem  28257  pythi  28281  normlem2  28544  normlem3  28545  normlem7  28549  normlem9  28551  bcseqi  28553  norm-ii-i  28570  normpythi  28575  normpari  28587  polid2i  28590  lnopunilem1  29445  lnophmlem2  29452  dpmul100  30171  dpadd3  30186  dpmul4  30188  ballotlem2  31153  hgt750lem2  31336  quad3  32165  faclimlem1  32227  itg2addnclem3  34093  sqmid3api  38155  235t711  38163  areaquad  38770  fourierswlem  41384  fouriersw  41385  2t6m3t4e0  43151