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

Theorem addcli 9078
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 9056 . 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 1725  (class class class)co 6067   CCcc 8972    + caddc 8977
This theorem is referenced by:  negdii  9368  eqneg  9718  nummac  10398  binom2i  11473  sqeqori  11476  crreczi  11487  nn0opthlem1  11544  nn0opth2i  11547  mod2xnegi  13390  karatsuba  13403  pige3  20408  eff1o  20434  1cubrlem  20664  1cubr  20665  bposlem8  21058  ipidsq  22192  ip1ilem  22310  pythi  22334  normlem2  22596  normlem3  22597  normlem7  22601  normlem9  22603  bcseqi  22605  norm-ii-i  22622  normpythi  22627  normpari  22639  polid2i  22642  lnopunilem1  23496  lnophmlem2  23503  ballotlem2  24729  faclimlem1  25346  ax5seglem7  25817  itg2addnclem3  26199
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addcl 9034
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator