Theorem addcli 11140

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

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11026   + caddc 11031

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

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

This theorem is referenced by:  eqneg  11863  2cn  12222  3cn  12228  4cn  12232  5cn  12235  6cn  12238  7cn  12241  8cn  12244  9cn  12247  nummac  12654  binom2i  14137  sqeqori  14139  crreczi  14153  nn0opthlem1  14193  nn0opth2i  14196  3dvds2dec  16262  mod2xnegi  17001  karatsuba  17013  pige3ALT  26487  eff1o  26516  1cubrlem  26809  1cubr  26810  bposlem8  27260  ax5seglem7  29010  ipidsq  30787  ip1ilem  30903  pythi  30927  normlem2  31188  normlem3  31189  normlem7  31193  normlem9  31195  bcseqi  31197  norm-ii-i  31214  normpythi  31219  normpari  31231  polid2i  31234  lnopunilem1  32087  lnophmlem2  32094  dpmul100  32980  dpadd3  32995  dpmul4  32997  cos9thpiminplylem4  33944  cos9thpiminplylem5  33945  ballotlem2  34648  hgt750lem2  34811  quad3  35866  faclimlem1  35939  itg2addnclem3  37876  sqmid3api  42559  235t711  42581  sn-0tie0  42727  fltnltalem  42926  areaquad  43479  resqrtvalex  43907  imsqrtvalex  43908  fourierswlem  46495  fouriersw  46496  2t6m3t4e0  48615