Theorem addcli 11246

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132   + caddc 11137

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

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

This theorem is referenced by:  eqneg  11966  2cn  12320  3cn  12326  4cn  12330  5cn  12333  6cn  12336  7cn  12339  8cn  12342  9cn  12345  nummac  12758  binom2i  14235  sqeqori  14237  crreczi  14251  nn0opthlem1  14291  nn0opth2i  14294  3dvds2dec  16357  mod2xnegi  17096  karatsuba  17108  pige3ALT  26486  eff1o  26515  1cubrlem  26808  1cubr  26809  bposlem8  27259  ax5seglem7  28919  ipidsq  30696  ip1ilem  30812  pythi  30836  normlem2  31097  normlem3  31098  normlem7  31102  normlem9  31104  bcseqi  31106  norm-ii-i  31123  normpythi  31128  normpari  31140  polid2i  31143  lnopunilem1  31996  lnophmlem2  32003  dpmul100  32876  dpadd3  32891  dpmul4  32893  cos9thpiminplylem4  33824  cos9thpiminplylem5  33825  ballotlem2  34526  hgt750lem2  34689  quad3  35697  faclimlem1  35765  itg2addnclem3  37702  sqmid3api  42300  235t711  42321  sn-0tie0  42449  fltnltalem  42652  areaquad  43207  resqrtvalex  43636  imsqrtvalex  43637  fourierswlem  46226  fouriersw  46227  2t6m3t4e0  48290