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

Theorem addcli 9125
Description: Closure law for addition. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1  |-  A  e.  CC
axi.2  |-  B  e.  CC
Assertion
Ref Expression
addcli  |-  ( A  +  B )  e.  CC

Proof of Theorem addcli
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 axi.2 . 2  |-  B  e.  CC
3 addcl 9103 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3mp2an 655 1  |-  ( A  +  B )  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1727  (class class class)co 6110   CCcc 9019    + caddc 9024
This theorem is referenced by:  negdii  9415  eqneg  9765  nummac  10445  binom2i  11521  sqeqori  11524  crreczi  11535  nn0opthlem1  11592  nn0opth2i  11595  mod2xnegi  13438  karatsuba  13451  pige3  20456  eff1o  20482  1cubrlem  20712  1cubr  20713  bposlem8  21106  ipidsq  22240  ip1ilem  22358  pythi  22382  normlem2  22644  normlem3  22645  normlem7  22649  normlem9  22651  bcseqi  22653  norm-ii-i  22670  normpythi  22675  normpari  22687  polid2i  22690  lnopunilem1  23544  lnophmlem2  23551  ballotlem2  24777  faclimlem1  25393  ax5seglem7  25905  itg2addnclem3  26296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 9081
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator