Theorem addcli 11146

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7362  ℂcc 11031   + caddc 11036

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

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

This theorem is referenced by:  eqneg  11870  2cn  12251  3cn  12257  4cn  12261  5cn  12264  6cn  12267  7cn  12270  8cn  12273  9cn  12276  nummac  12684  binom2i  14169  sqeqori  14171  crreczi  14185  nn0opthlem1  14225  nn0opth2i  14228  3dvds2dec  16297  mod2xnegi  17037  karatsuba  17049  pige3ALT  26501  eff1o  26530  1cubrlem  26822  1cubr  26823  bposlem8  27272  ax5seglem7  29022  ipidsq  30800  ip1ilem  30916  pythi  30940  normlem2  31201  normlem3  31202  normlem7  31206  normlem9  31208  bcseqi  31210  norm-ii-i  31227  normpythi  31232  normpari  31244  polid2i  31247  lnopunilem1  32100  lnophmlem2  32107  dpmul100  32975  dpadd3  32990  dpmul4  32992  cos9thpiminplylem4  33949  cos9thpiminplylem5  33950  ballotlem2  34653  hgt750lem2  34816  quad3  35872  faclimlem1  35945  itg2addnclem3  38012  sqmid3api  42733  235t711  42755  sn-0tie0  42914  fltnltalem  43113  areaquad  43666  resqrtvalex  44094  imsqrtvalex  44095  fourierswlem  46680  fouriersw  46681  2t6m3t4e0  48840