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

Theorem addcld 9636
Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1
addcld.2
Assertion
Ref Expression
addcld

Proof of Theorem addcld
StepHypRef Expression
1 addcld.1 . 2
2 addcld.2 . 2
3 addcl 9595 . 2
41, 2, 3syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  (class class class)co 6296   cc 9511   caddc 9516
This theorem is referenced by:  cnegex  9782  addcom  9787  addcomd  9803  negeu  9833  addsubass  9853  subsub2  9870  subsub4  9875  pnpcan  9881  pnncan  9883  addsub4  9885  pnpncand  10006  divdir  10255  cju  10557  cnref1o  11244  xov1plusxeqvd  11695  expaddz  12210  binom3  12287  spllen  12730  crre  12947  remullem  12961  imval2  12984  cjreim2  12994  sqreulem  13192  addcn2  13416  o1add  13436  fsumadd  13561  isumadd  13582  binomlem  13641  efaddlem  13828  ef4p  13848  cosf  13860  tanval2  13868  tanval3  13869  resin4p  13873  recos4p  13874  efival  13887  sinadd  13899  cosadd  13900  tanadd  13902  sadadd2lem2  14100  sadadd2lem  14109  pythagtriplem1  14340  pythagtriplem12  14350  pythagtriplem17  14355  pcbc  14419  mul4sqlem  14471  4sqlem14  14476  vdwlem6  14504  vdwlem9  14507  mulgdirlem  16166  blcvx  21303  tchcphlem1  21678  csbren  21826  ovollb2lem  21899  mbfadd  22068  itgcnlem  22196  itgaddlem2  22230  dvmptre  22372  dvsincos  22382  taylthlem2  22769  ptolemy  22889  tanregt0  22926  eff1olem  22935  cosargd  22993  tanarg  23004  logf1o2  23031  efopn  23039  cxpsqrtlem  23083  cxpeq  23131  ang180lem1  23141  ang180lem2  23142  ang180lem3  23143  ang180lem4  23144  pythag  23149  ssscongptld  23156  chordthmlem  23163  chordthmlem2  23164  chordthmlem3  23165  chordthmlem4  23166  chordthmlem5  23167  heron  23169  quad2  23170  dcubic1lem  23174  dcubic2  23175  dcubic1  23176  dcubic  23177  mcubic  23178  cubic2  23179  cubic  23180  binom4  23181  dquartlem1  23182  dquartlem2  23183  dquart  23184  quart1cl  23185  quart1lem  23186  quart1  23187  quartlem1  23188  quartlem2  23189  quartlem3  23190  quartlem4  23191  quart  23192  asinlem3  23202  asinf  23203  asinneg  23217  efiasin  23219  asinsinlem  23222  asinsin  23223  asinbnd  23230  atanlogaddlem  23244  ftalem7  23352  basellem3  23356  bposlem9  23567  lgsquad2lem1  23633  dchrvmasumiflem2  23687  mulogsumlem  23716  mulog2sumlem1  23719  mulog2sumlem2  23720  mulog2sumlem3  23721  selberglem1  23730  selberg2  23736  selberg3lem1  23742  selbergr  23753  selberg3r  23754  pntrlog2bndlem1  23762  pntrlog2bndlem2  23763  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntrlog2bnd  23769  brbtwn2  24208  colinearalglem1  24209  colinearalglem2  24210  axeuclidlem  24265  axcontlem2  24268  axcontlem7  24273  axcontlem8  24274  4ipval2  25618  4ipval3  25622  dipcj  25627  golem1  27190  lt2addrd  27563  bhmafibid1  27632  bhmafibid2  27633  2sqmod  27636  archirngz  27733  archiabllem2c  27739  cnre2csqima  27893  ballotlemsima  28454  dmgmaddnn0  28569  dmgmdivn0  28570  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem4  28574  lgamgulmlem5  28575  lgamgulmlem6  28576  lgamgulm2  28578  lgambdd  28579  lgamucov  28580  lgamcvg2  28597  gamcvg  28598  gamcvg2lem  28601  iprodgam  29125  binomfallfaclem2  29162  bpoly4  29821  fsumcube  29822  itg2addnclem3  30068  itgaddnclem2  30074  itgaddnc  30075  ftc1anclem6  30095  ftc1anclem8  30097  dvasin  30103  areacirclem1  30107  areacirclem4  30110  areacirc  30112  pellexlem2  30766  pellexlem6  30770  pell1234qrreccl  30790  pell1234qrmulcl  30791  pell14qrdich  30805  rmxyneg  30856  rmxyadd  30857  jm2.19lem4  30934  jm2.26lem3  30943  itgpowd  31182  binomcxplemnn0  31254  binomcxplemrat  31255  binomcxplemfrat  31256  binomcxplemdvbinom  31258  binomcxplemnotnn0  31261  sub2times  31455  clim1fr1  31607  limcperiod  31634  addlimc  31654  coseq0  31664  dvxpaek  31737  dvnxpaek  31739  dvnmul  31740  itgiccshift  31779  itgperiod  31780  stoweidlem1  31783  stoweidlem11  31793  stoweidlem13  31795  wallispilem4  31850  wallispilem5  31851  wallispi  31852  wallispi2lem1  31853  wallispi2lem2  31854  wallispi2  31855  stirlinglem1  31856  stirlinglem3  31858  stirlinglem4  31859  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem10  31865  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  stirlinglem15  31870  dirkerper  31878  dirkertrigeqlem1  31880  dirkertrigeqlem2  31881  dirkertrigeqlem3  31882  dirkeritg  31884  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem18  31907  fourierdlem26  31915  fourierdlem30  31919  fourierdlem48  31937  fourierdlem49  31938  fourierdlem79  31968  fourierdlem83  31972  fourierdlem92  31981  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  sigaraf  32070  sigaras  32072  sinhpcosh  33134  int-rightdistd  38001
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