Theorem addcli 11186

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7389  ℂcc 11072   + caddc 11077

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

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

This theorem is referenced by:  eqneg  11908  2cn  12262  3cn  12268  4cn  12272  5cn  12275  6cn  12278  7cn  12281  8cn  12284  9cn  12287  nummac  12700  binom2i  14183  sqeqori  14185  crreczi  14199  nn0opthlem1  14239  nn0opth2i  14242  3dvds2dec  16309  mod2xnegi  17048  karatsuba  17060  pige3ALT  26435  eff1o  26464  1cubrlem  26757  1cubr  26758  bposlem8  27208  ax5seglem7  28868  ipidsq  30645  ip1ilem  30761  pythi  30785  normlem2  31046  normlem3  31047  normlem7  31051  normlem9  31053  bcseqi  31055  norm-ii-i  31072  normpythi  31077  normpari  31089  polid2i  31092  lnopunilem1  31945  lnophmlem2  31952  dpmul100  32823  dpadd3  32838  dpmul4  32840  cos9thpiminplylem4  33781  cos9thpiminplylem5  33782  ballotlem2  34486  hgt750lem2  34649  quad3  35657  faclimlem1  35725  itg2addnclem3  37662  sqmid3api  42266  235t711  42288  sn-0tie0  42434  fltnltalem  42643  areaquad  43198  resqrtvalex  43627  imsqrtvalex  43628  fourierswlem  46221  fouriersw  46222  2t6m3t4e0  48326