Theorem addcli 11121

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   + caddc 11012

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

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

This theorem is referenced by:  eqneg  11844  2cn  12203  3cn  12209  4cn  12213  5cn  12216  6cn  12219  7cn  12222  8cn  12225  9cn  12228  nummac  12636  binom2i  14119  sqeqori  14121  crreczi  14135  nn0opthlem1  14175  nn0opth2i  14178  3dvds2dec  16244  mod2xnegi  16983  karatsuba  16995  pige3ALT  26427  eff1o  26456  1cubrlem  26749  1cubr  26750  bposlem8  27200  ax5seglem7  28880  ipidsq  30654  ip1ilem  30770  pythi  30794  normlem2  31055  normlem3  31056  normlem7  31060  normlem9  31062  bcseqi  31064  norm-ii-i  31081  normpythi  31086  normpari  31098  polid2i  31101  lnopunilem1  31954  lnophmlem2  31961  dpmul100  32838  dpadd3  32853  dpmul4  32855  cos9thpiminplylem4  33758  cos9thpiminplylem5  33759  ballotlem2  34463  hgt750lem2  34626  quad3  35653  faclimlem1  35726  itg2addnclem3  37663  sqmid3api  42266  235t711  42288  sn-0tie0  42434  fltnltalem  42645  areaquad  43199  resqrtvalex  43628  imsqrtvalex  43629  fourierswlem  46221  fouriersw  46222  2t6m3t4e0  48342