Theorem addcli 9923

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

Syntax hints:   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818

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

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  eqneg  10624  nummac  11434  binom2i  12836  sqeqori  12838  crreczi  12851  nn0opthlem1  12917  nn0opth2i  12920  3dvds2dec  14894  3dvds2decOLD  14895  mod2xnegi  15613  karatsuba  15630  karatsubaOLD  15631  pige3  24073  eff1o  24099  1cubrlem  24368  1cubr  24369  bposlem8  24816  ax5seglem7  25615  ipidsq  26949  ip1ilem  27065  pythi  27089  normlem2  27352  normlem3  27353  normlem7  27357  normlem9  27359  bcseqi  27361  norm-ii-i  27378  normpythi  27383  normpari  27395  polid2i  27398  lnopunilem1  28253  lnophmlem2  28260  ballotlem2  29877  quad3  30818  faclimlem1  30882  itg2addnclem3  32633  areaquad  36821  fourierswlem  39123  fouriersw  39124  2t6m3t4e0  41919