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

Theorem addcli 9020
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 8998 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3mp2an 654 1  |-  ( A  +  B )  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1717  (class class class)co 6013   CCcc 8914    + caddc 8919
This theorem is referenced by:  negdii  9309  eqneg  9659  nummac  10339  binom2i  11410  sqeqori  11413  crreczi  11424  nn0opthlem1  11481  nn0opth2i  11484  mod2xnegi  13327  karatsuba  13340  pige3  20285  eff1o  20311  1cubrlem  20541  1cubr  20542  bposlem8  20935  ipidsq  22050  ip1ilem  22168  pythi  22192  normlem2  22454  normlem3  22455  normlem7  22459  normlem9  22461  bcseqi  22463  norm-ii-i  22480  normpythi  22485  normpari  22497  polid2i  22500  lnopunilem1  23354  lnophmlem2  23361  ballotlem2  24518  faclimlem1  25113  ax5seglem7  25581  itg2addnc  25952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addcl 8976
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator