Theorem addcli 11156

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   + caddc 11047

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

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

This theorem is referenced by:  eqneg  11878  2cn  12237  3cn  12243  4cn  12247  5cn  12250  6cn  12253  7cn  12256  8cn  12259  9cn  12262  nummac  12670  binom2i  14153  sqeqori  14155  crreczi  14169  nn0opthlem1  14209  nn0opth2i  14212  3dvds2dec  16279  mod2xnegi  17018  karatsuba  17030  pige3ALT  26462  eff1o  26491  1cubrlem  26784  1cubr  26785  bposlem8  27235  ax5seglem7  28915  ipidsq  30689  ip1ilem  30805  pythi  30829  normlem2  31090  normlem3  31091  normlem7  31095  normlem9  31097  bcseqi  31099  norm-ii-i  31116  normpythi  31121  normpari  31133  polid2i  31136  lnopunilem1  31989  lnophmlem2  31996  dpmul100  32867  dpadd3  32882  dpmul4  32884  cos9thpiminplylem4  33768  cos9thpiminplylem5  33769  ballotlem2  34473  hgt750lem2  34636  quad3  35650  faclimlem1  35723  itg2addnclem3  37660  sqmid3api  42264  235t711  42286  sn-0tie0  42432  fltnltalem  42643  areaquad  43198  resqrtvalex  43627  imsqrtvalex  43628  fourierswlem  46221  fouriersw  46222  2t6m3t4e0  48329