Theorem addcli 11268

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

Syntax hints:   ∈ wcel 2107  (class class class)co 7432  ℂcc 11154   + caddc 11159

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

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

This theorem is referenced by:  eqneg  11988  2cn  12342  3cn  12348  4cn  12352  5cn  12355  6cn  12358  7cn  12361  8cn  12364  9cn  12367  nummac  12780  binom2i  14252  sqeqori  14254  crreczi  14268  nn0opthlem1  14308  nn0opth2i  14311  3dvds2dec  16371  mod2xnegi  17110  karatsuba  17122  pige3ALT  26563  eff1o  26592  1cubrlem  26885  1cubr  26886  bposlem8  27336  ax5seglem7  28951  ipidsq  30730  ip1ilem  30846  pythi  30870  normlem2  31131  normlem3  31132  normlem7  31136  normlem9  31138  bcseqi  31140  norm-ii-i  31157  normpythi  31162  normpari  31174  polid2i  31177  lnopunilem1  32030  lnophmlem2  32037  dpmul100  32880  dpadd3  32895  dpmul4  32897  ballotlem2  34492  hgt750lem2  34668  quad3  35676  faclimlem1  35744  itg2addnclem3  37681  sqmid3api  42323  235t711  42344  sn-0tie0  42474  fltnltalem  42677  areaquad  43233  resqrtvalex  43663  imsqrtvalex  43664  fourierswlem  46250  fouriersw  46251  2t6m3t4e0  48269