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

Theorem addcli 9382
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 9356 . 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 1756  (class class class)co 6086   CCcc 9272    + caddc 9277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 9334
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  negdii  9684  eqneg  10043  nummac  10779  binom2i  11967  sqeqori  11970  crreczi  11981  nn0opthlem1  12038  nn0opth2i  12041  mod2xnegi  14092  karatsuba  14105  pige3  21954  eff1o  21980  1cubrlem  22211  1cubr  22212  bposlem8  22605  ax5seglem7  23132  ipidsq  24059  ip1ilem  24177  pythi  24201  normlem2  24464  normlem3  24465  normlem7  24469  normlem9  24471  bcseqi  24473  norm-ii-i  24490  normpythi  24495  normpari  24507  polid2i  24510  lnopunilem1  25365  lnophmlem2  25372  ballotlem2  26823  faclimlem1  27500  itg2addnclem3  28398  areaquad  29545  2t6m3t4e0  30692
  Copyright terms: Public domain W3C validator