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

Theorem addcli 9589
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 9563 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3mp2an 672 1  |-  ( A  +  B )  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762  (class class class)co 6275   CCcc 9479    + caddc 9484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 9541
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  negdii  9892  eqneg  10253  nummac  10997  binom2i  12232  sqeqori  12235  crreczi  12246  nn0opthlem1  12303  nn0opth2i  12306  mod2xnegi  14405  karatsuba  14418  pige3  22636  eff1o  22662  1cubrlem  22893  1cubr  22894  bposlem8  23287  ax5seglem7  23907  ipidsq  25285  ip1ilem  25403  pythi  25427  normlem2  25690  normlem3  25691  normlem7  25695  normlem9  25697  bcseqi  25699  norm-ii-i  25716  normpythi  25721  normpari  25733  polid2i  25736  lnopunilem1  26591  lnophmlem2  26598  ballotlem2  28053  quad3  28485  faclimlem1  28731  itg2addnclem3  29632  areaquad  30778  fourierswlem  31486  fouriersw  31487  2t6m3t4e0  31876
  Copyright terms: Public domain W3C validator