Theorem addcli 11242

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

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℂcc 11125   + caddc 11130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 11187

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  eqneg  11962  2cn  12343  3cn  12349  4cn  12353  5cn  12356  6cn  12359  7cn  12362  8cn  12365  9cn  12368  nummac  12789  binom2i  14279  sqeqori  14281  crreczi  14295  nn0opthlem1  14335  nn0opth2i  14338  3dvds2dec  16426  mod2xnegi  17166  karatsuba  17178  pige3ALT  26760  eff1o  26789  1cubrlem  27081  1cubr  27082  bposlem8  27530  ax5seglem7  29395  ipidsq  31194  ip1ilem  31310  pythi  31334  normlem2  31595  normlem3  31596  normlem7  31600  normlem9  31602  bcseqi  31604  norm-ii-i  31621  normpythi  31626  normpari  31638  polid2i  31641  lnopunilem1  32494  lnophmlem2  32501  dpmul100  33345  dpadd3  33360  dpmul4  33362  cos9thpiminplylem4  34298  cos9thpiminplylem5  34299  ballotlem2  35003  hgt750lem2  35163  quad3  36252  faclimlem1  36325  itg2addnclem3  38425  25or6to4  43075  sqmid3api  43161  235t711  43183  sn-0tie0  43342  fltnltalem  43511  areaquad  44060  resqrtvalex  44488  imsqrtvalex  44489  fourierswlem  47061  fouriersw  47062  goldpolyfactor  47748  goldratmolem3  47755  goldratmolem4  47756  goldratval  47757  2t6m3t4e0  49281