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

Theorem addcli 9630
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 9604 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3mp2an 670 1  |-  ( A  +  B )  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842  (class class class)co 6278   CCcc 9520    + caddc 9525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 9582
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  negdiiOLD  9940  eqneg  10305  nummac  11051  binom2i  12322  sqeqori  12324  crreczi  12335  nn0opthlem1  12392  nn0opth2i  12395  mod2xnegi  14766  karatsuba  14779  pige3  23202  eff1o  23228  1cubrlem  23497  1cubr  23498  bposlem8  23947  ax5seglem7  24655  ipidsq  26037  ip1ilem  26155  pythi  26179  normlem2  26442  normlem3  26443  normlem7  26447  normlem9  26449  bcseqi  26451  norm-ii-i  26468  normpythi  26473  normpari  26485  polid2i  26488  lnopunilem1  27342  lnophmlem2  27349  ballotlem2  28933  quad3  29876  faclimlem1  29952  itg2addnclem3  31441  areaquad  35548  fourierswlem  37381  fouriersw  37382  2t6m3t4e0  38448
  Copyright terms: Public domain W3C validator