Theorem addcli 11118

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

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004   + caddc 11009

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

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

This theorem is referenced by:  eqneg  11841  2cn  12200  3cn  12206  4cn  12210  5cn  12213  6cn  12216  7cn  12219  8cn  12222  9cn  12225  nummac  12633  binom2i  14119  sqeqori  14121  crreczi  14135  nn0opthlem1  14175  nn0opth2i  14178  3dvds2dec  16244  mod2xnegi  16983  karatsuba  16995  pige3ALT  26456  eff1o  26485  1cubrlem  26778  1cubr  26779  bposlem8  27229  ax5seglem7  28913  ipidsq  30690  ip1ilem  30806  pythi  30830  normlem2  31091  normlem3  31092  normlem7  31096  normlem9  31098  bcseqi  31100  norm-ii-i  31117  normpythi  31122  normpari  31134  polid2i  31137  lnopunilem1  31990  lnophmlem2  31997  dpmul100  32877  dpadd3  32892  dpmul4  32894  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  ballotlem2  34502  hgt750lem2  34665  quad3  35714  faclimlem1  35787  itg2addnclem3  37723  sqmid3api  42386  235t711  42408  sn-0tie0  42554  fltnltalem  42765  areaquad  43319  resqrtvalex  43748  imsqrtvalex  43749  fourierswlem  46338  fouriersw  46339  2t6m3t4e0  48458