Theorem addcli 10636

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

Syntax hints:   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529

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

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

This theorem is referenced by:  eqneg  11349  2cn  11700  3cn  11706  4cn  11710  5cn  11713  6cn  11716  7cn  11719  8cn  11722  9cn  11725  nummac  12131  binom2i  13570  sqeqori  13572  crreczi  13585  nn0opthlem1  13624  nn0opth2i  13627  3dvds2dec  15674  mod2xnegi  16397  karatsuba  16410  pige3ALT  25112  eff1o  25141  1cubrlem  25427  1cubr  25428  bposlem8  25875  ax5seglem7  26729  ipidsq  28493  ip1ilem  28609  pythi  28633  normlem2  28894  normlem3  28895  normlem7  28899  normlem9  28901  bcseqi  28903  norm-ii-i  28920  normpythi  28925  normpari  28937  polid2i  28940  lnopunilem1  29793  lnophmlem2  29800  dpmul100  30599  dpadd3  30614  dpmul4  30616  ballotlem2  31856  hgt750lem2  32033  quad3  33026  faclimlem1  33088  itg2addnclem3  35110  sqmid3api  39477  235t711  39485  sn-0tie0  39576  fltnltalem  39618  areaquad  40166  resqrtvalex  40345  imsqrtvalex  40346  fourierswlem  42872  fouriersw  42873  2t6m3t4e0  44750