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

Theorem addcl 9595
Description: Alias for ax-addcl 9573, for naming consistency with addcli 9621. Use this theorem instead of ax-addcl 9573 or axaddcl 9549. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addcl

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 9573 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  (class class class)co 6296   cc 9511   caddc 9516
This theorem is referenced by:  adddir  9608  0cn  9609  addcli  9621  addcld  9636  muladd11  9771  peano2cn  9773  add4  9817  0cnALT  9832  negeu  9833  pncan  9849  2addsub  9857  addsubeq4  9858  nppcan2  9873  ppncan  9884  muladd  10014  mulsub  10024  recex  10206  muleqadd  10218  conjmul  10286  halfaddsubcl  10796  halfaddsub  10797  uzindOLD  10982  serf  12135  seradd  12149  sersub  12150  binom3  12287  bernneq  12292  lswccatn0lsw  12607  revccat  12740  2cshwcshw  12793  shftlem  12901  shftval2  12908  shftval5  12911  2shfti  12913  crre  12947  crim  12948  cjadd  12974  addcj  12981  sqabsadd  13115  absreimsq  13125  absreim  13126  abstri  13163  sqreulem  13192  sqreu  13193  addcn2  13416  o1add  13436  climadd  13454  clim2ser  13477  clim2ser2  13478  isermulc2  13480  isercolllem3  13489  summolem3  13536  summolem2a  13537  fsumcl  13555  fsummulc2  13599  fsumrelem  13621  binom  13642  isumsplit  13652  efcj  13827  ef4p  13848  tanval3  13869  efi4p  13872  sinadd  13899  cosadd  13900  tanadd  13902  addsin  13905  demoivreALT  13936  opoe  14335  pythagtriplem4  14343  pythagtriplem12  14350  pythagtriplem14  14352  pythagtriplem16  14354  gzaddcl  14455  cnaddablx  16874  cnaddabl  16875  cncrng  18439  cnperf  21325  dvaddbr  22341  dvaddf  22345  dveflem  22380  plyaddcl  22617  plymulcl  22618  plysubcl  22619  coeaddlem  22646  dgrcolem1  22670  dgrcolem2  22671  quotlem  22696  quotcl2  22698  quotdgr  22699  sinperlem  22873  ptolemy  22889  tangtx  22898  sinkpi  22912  efif1olem2  22930  logrnaddcl  22962  logneg  22972  logimul  22999  cxpadd  23060  binom4  23181  atanf  23211  atanneg  23238  atancj  23241  efiatan  23243  atanlogaddlem  23244  atanlogadd  23245  atanlogsublem  23246  atanlogsub  23247  efiatan2  23248  2efiatan  23249  tanatan  23250  cosatan  23252  cosatanne0  23253  atantan  23254  atanbndlem  23256  atans2  23262  dvatan  23266  atantayl  23268  efrlim  23299  dfef2  23300  ftalem7  23352  prmorcht  23452  bposlem9  23567  lgsquad2lem1  23633  2sqlem2  23639  wlkdvspthlem  24609  wwlkext2clwwlk  24803  gxadd  25277  cncph  25734  hhssnv  26180  hoadddir  26723  superpos  27273  gamcvg2lem  28601  risefacval2  29132  risefaccl  29137  risefallfac  29146  risefacp1  29151  binomfallfac  29163  binomrisefac  29164  bpoly3  29820  cos2h  30046  tan2h  30047  dvtanlem  30064  ftc1anclem3  30092  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  stirlinglem5  31860  stirlinglem7  31862  cnapbmcpd  32316
This theorem was proved from axioms:  ax-addcl 9573
  Copyright terms: Public domain W3C validator