Theorem addcli 11232

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

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115   + caddc 11120

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

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

This theorem is used by:  eqneg  11952  2cn  12333  3cn  12339  4cn  12343  5cn  12346  6cn  12349  7cn  12352  8cn  12355  9cn  12358  nummac  12779  binom2i  14268  sqeqori  14270  crreczi  14284  nn0opthlem1  14324  nn0opth2i  14327  3dvds2dec  16415  mod2xnegi  17155  karatsuba  17167  pige3ALT  26738  eff1o  26767  1cubrlem  27059  1cubr  27060  bposlem8  27508  ax5seglem7  29342  ipidsq  31135  ip1ilem  31251  pythi  31275  normlem2  31536  normlem3  31537  normlem7  31541  normlem9  31543  bcseqi  31545  norm-ii-i  31562  normpythi  31567  normpari  31579  polid2i  31582  lnopunilem1  32435  lnophmlem2  32442  dpmul100  33288  dpadd3  33303  dpmul4  33305  cos9thpiminplylem4  34241  cos9thpiminplylem5  34242  ballotlem2  34946  hgt750lem2  35106  quad3  36201  faclimlem1  36274  itg2addnclem3  38383  25or6to4  43033  sqmid3api  43104  235t711  43126  sn-0tie0  43285  fltnltalem  43454  areaquad  44003  resqrtvalex  44431  imsqrtvalex  44432  fourierswlem  47004  fouriersw  47005  2t6m3t4e0  49187