Theorem addcli 11315

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

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198   + caddc 11203

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

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

This theorem is used by:  eqneg  12037  2cn  12418  3cn  12424  4cn  12428  5cn  12431  6cn  12434  7cn  12437  8cn  12440  9cn  12443  nummac  12864  binom2i  14356  sqeqori  14358  crreczi  14372  nn0opthlem1  14412  nn0opth2i  14415  3dvds2dec  16503  mod2xnegi  17249  karatsuba  17261  pige3ALT  26848  eff1o  26877  1cubrlem  27169  1cubr  27170  bposlem8  27618  ax5seglem7  29513  ipidsq  31312  ip1ilem  31428  pythi  31452  normlem2  31713  normlem3  31714  normlem7  31718  normlem9  31720  bcseqi  31722  norm-ii-i  31739  normpythi  31744  normpari  31756  polid2i  31759  lnopunilem1  32612  lnophmlem2  32619  dpmul100  33463  dpadd3  33478  dpmul4  33480  cos9thpiminplylem4  34417  cos9thpiminplylem5  34418  ballotlem2  35121  hgt750lem2  35281  quad3  36435  faclimlem1  36508  itg2addnclem3  38591  25or6to4  43256  sqmid3api  43340  235t711  43362  sn-0tie0  43515  fltnltalem  43673  areaquad  44217  resqrtvalex  44644  imsqrtvalex  44645  fourierswlem  47239  fouriersw  47240  goldpolyfactor  47926  goldratmolem3  47933  goldratmolem4  47934  goldratval  47935  2t6m3t4e0  49459