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

Theorem addcli 8841
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 8819 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3mp2an 653 1  |-  ( A  +  B )  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740
This theorem is referenced by:  negdii  9130  eqneg  9480  nummac  10156  binom2i  11212  sqeqori  11215  crreczi  11226  nn0opthlem1  11283  nn0opth2i  11286  mod2xnegi  13086  karatsuba  13099  pige3  19885  eff1o  19911  1cubrlem  20137  1cubr  20138  bposlem8  20530  ipidsq  21286  ip1ilem  21404  pythi  21428  normlem2  21690  normlem3  21691  normlem7  21695  normlem9  21697  bcseqi  21699  norm-ii-i  21716  normpythi  21721  normpari  21733  polid2i  21736  lnopunilem1  22590  lnophmlem2  22597  ballotlem2  23047  ax5seglem7  24563
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addcl 8797
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator