Theorem addcli 11244

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

Syntax hints:   ∈ wcel 2099  (class class class)co 7414  ℂcc 11130   + caddc 11135

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

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

This theorem is referenced by:  eqneg  11958  2cn  12311  3cn  12317  4cn  12321  5cn  12324  6cn  12327  7cn  12330  8cn  12333  9cn  12336  nummac  12746  binom2i  14201  sqeqori  14203  crreczi  14216  nn0opthlem1  14253  nn0opth2i  14256  3dvds2dec  16303  mod2xnegi  17033  karatsuba  17046  pige3ALT  26447  eff1o  26476  1cubrlem  26766  1cubr  26767  bposlem8  27217  ax5seglem7  28739  ipidsq  30513  ip1ilem  30629  pythi  30653  normlem2  30914  normlem3  30915  normlem7  30919  normlem9  30921  bcseqi  30923  norm-ii-i  30940  normpythi  30945  normpari  30957  polid2i  30960  lnopunilem1  31813  lnophmlem2  31820  dpmul100  32614  dpadd3  32629  dpmul4  32631  ballotlem2  34098  hgt750lem2  34274  quad3  35264  faclimlem1  35327  itg2addnclem3  37135  sqmid3api  41829  235t711  41839  sn-0tie0  41966  fltnltalem  42058  areaquad  42616  resqrtvalex  43047  imsqrtvalex  43048  fourierswlem  45590  fouriersw  45591  2t6m3t4e0  47384