Theorem addcli 11249

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

Syntax hints:   ∈ wcel 2107  (class class class)co 7413  ℂcc 11135   + caddc 11140

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

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

This theorem is referenced by:  eqneg  11969  2cn  12323  3cn  12329  4cn  12333  5cn  12336  6cn  12339  7cn  12342  8cn  12345  9cn  12348  nummac  12761  binom2i  14233  sqeqori  14235  crreczi  14249  nn0opthlem1  14289  nn0opth2i  14292  3dvds2dec  16352  mod2xnegi  17091  karatsuba  17103  pige3ALT  26498  eff1o  26527  1cubrlem  26820  1cubr  26821  bposlem8  27271  ax5seglem7  28880  ipidsq  30657  ip1ilem  30773  pythi  30797  normlem2  31058  normlem3  31059  normlem7  31063  normlem9  31065  bcseqi  31067  norm-ii-i  31084  normpythi  31089  normpari  31101  polid2i  31104  lnopunilem1  31957  lnophmlem2  31964  dpmul100  32819  dpadd3  32834  dpmul4  32836  ballotlem2  34450  hgt750lem2  34626  quad3  35634  faclimlem1  35702  itg2addnclem3  37639  sqmid3api  42281  235t711  42302  sn-0tie0  42432  fltnltalem  42635  areaquad  43191  resqrtvalex  43620  imsqrtvalex  43621  fourierswlem  46202  fouriersw  46203  2t6m3t4e0  48222