Theorem addcli 11292

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

Syntax hints:   ∈ wcel 2103  (class class class)co 7445  ℂcc 11178   + caddc 11183

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

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

This theorem is referenced by:  eqneg  12010  2cn  12364  3cn  12370  4cn  12374  5cn  12377  6cn  12380  7cn  12383  8cn  12386  9cn  12389  nummac  12799  binom2i  14257  sqeqori  14259  crreczi  14273  nn0opthlem1  14313  nn0opth2i  14316  3dvds2dec  16375  mod2xnegi  17113  karatsuba  17126  pige3ALT  26571  eff1o  26600  1cubrlem  26893  1cubr  26894  bposlem8  27344  ax5seglem7  28959  ipidsq  30733  ip1ilem  30849  pythi  30873  normlem2  31134  normlem3  31135  normlem7  31139  normlem9  31141  bcseqi  31143  norm-ii-i  31160  normpythi  31165  normpari  31177  polid2i  31180  lnopunilem1  32033  lnophmlem2  32040  dpmul100  32853  dpadd3  32868  dpmul4  32870  ballotlem2  34445  hgt750lem2  34621  quad3  35630  faclimlem1  35697  itg2addnclem3  37581  sqmid3api  42220  235t711  42230  sn-0tie0  42348  fltnltalem  42550  areaquad  43117  resqrtvalex  43547  imsqrtvalex  43548  fourierswlem  46085  fouriersw  46086  2t6m3t4e0  47991