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

Theorem addcli 8857
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 8835 . 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 1696  (class class class)co 5874   CCcc 8751    + caddc 8756
This theorem is referenced by:  negdii  9146  eqneg  9496  nummac  10172  binom2i  11228  sqeqori  11231  crreczi  11242  nn0opthlem1  11299  nn0opth2i  11302  mod2xnegi  13102  karatsuba  13115  pige3  19901  eff1o  19927  1cubrlem  20153  1cubr  20154  bposlem8  20546  ipidsq  21302  ip1ilem  21420  pythi  21444  normlem2  21706  normlem3  21707  normlem7  21711  normlem9  21713  bcseqi  21715  norm-ii-i  21732  normpythi  21737  normpari  21749  polid2i  21752  lnopunilem1  22606  lnophmlem2  22613  ballotlem2  23063  ax5seglem7  24635  itg2addnc  25005
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addcl 8813
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator