MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcli Structured version   Visualization version   GIF version

Theorem addcli 10256
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
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 axi.2 . 2 𝐵 ∈ ℂ
3 addcl 10230 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
41, 2, 3mp2an 710 1 (𝐴 + 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2139  (class class class)co 6814  cc 10146   + caddc 10151
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10208
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  eqneg  10957  nummac  11770  binom2i  13188  sqeqori  13190  crreczi  13203  nn0opthlem1  13269  nn0opth2i  13272  3dvds2dec  15278  3dvds2decOLD  15279  mod2xnegi  15997  karatsuba  16014  karatsubaOLD  16015  pige3  24489  eff1o  24515  1cubrlem  24788  1cubr  24789  bposlem8  25236  ax5seglem7  26035  ipidsq  27895  ip1ilem  28011  pythi  28035  normlem2  28298  normlem3  28299  normlem7  28303  normlem9  28305  bcseqi  28307  norm-ii-i  28324  normpythi  28329  normpari  28341  polid2i  28344  lnopunilem1  29199  lnophmlem2  29206  dpmul100  29935  dpadd3  29950  dpmul4  29952  ballotlem2  30880  hgt750lem2  31060  quad3  31892  faclimlem1  31957  itg2addnclem3  33794  areaquad  38322  fourierswlem  40968  fouriersw  40969  2t6m3t4e0  42654
  Copyright terms: Public domain W3C validator