Theorem addcli 11265

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

Syntax hints:   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151   + caddc 11156

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

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

This theorem is referenced by:  eqneg  11985  2cn  12339  3cn  12345  4cn  12349  5cn  12352  6cn  12355  7cn  12358  8cn  12361  9cn  12364  nummac  12776  binom2i  14248  sqeqori  14250  crreczi  14264  nn0opthlem1  14304  nn0opth2i  14307  3dvds2dec  16367  mod2xnegi  17105  karatsuba  17118  pige3ALT  26577  eff1o  26606  1cubrlem  26899  1cubr  26900  bposlem8  27350  ax5seglem7  28965  ipidsq  30739  ip1ilem  30855  pythi  30879  normlem2  31140  normlem3  31141  normlem7  31145  normlem9  31147  bcseqi  31149  norm-ii-i  31166  normpythi  31171  normpari  31183  polid2i  31186  lnopunilem1  32039  lnophmlem2  32046  dpmul100  32864  dpadd3  32879  dpmul4  32881  ballotlem2  34470  hgt750lem2  34646  quad3  35655  faclimlem1  35723  itg2addnclem3  37660  sqmid3api  42297  235t711  42318  sn-0tie0  42446  fltnltalem  42649  areaquad  43205  resqrtvalex  43635  imsqrtvalex  43636  fourierswlem  46186  fouriersw  46187  2t6m3t4e0  48193