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

Theorem addcli 9621
Description: Closure law for addition. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1
axi.2
Assertion
Ref Expression
addcli

Proof of Theorem addcli
StepHypRef Expression
1 axi.1 . 2
2 axi.2 . 2
3 addcl 9595 . 2
41, 2, 3mp2an 672 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  (class class class)co 6296   cc 9511   caddc 9516
This theorem is referenced by:  negdiiOLD  9927  eqneg  10289  nummac  11036  binom2i  12277  sqeqori  12280  crreczi  12291  nn0opthlem1  12348  nn0opth2i  12351  mod2xnegi  14557  karatsuba  14570  pige3  22910  eff1o  22936  1cubrlem  23172  1cubr  23173  bposlem8  23566  ax5seglem7  24238  ipidsq  25623  ip1ilem  25741  pythi  25765  normlem2  26028  normlem3  26029  normlem7  26033  normlem9  26035  bcseqi  26037  norm-ii-i  26054  normpythi  26059  normpari  26071  polid2i  26074  lnopunilem1  26929  lnophmlem2  26936  ballotlem2  28427  quad3  29024  faclimlem1  29168  itg2addnclem3  30068  areaquad  31184  fourierswlem  32013  fouriersw  32014  2t6m3t4e0  32937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 9573
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator