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

Theorem readdcl 9596
Description: Alias for ax-addrcl 9574, for naming consistency with readdcli 9630. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
readdcl

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 9574 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  (class class class)co 6296   cr 9512   caddc 9516
This theorem is referenced by:  0re  9617  readdcli  9630  readdcld  9644  axltadd  9679  peano2re  9774  00id  9776  resubcl  9906  ltaddsub  10051  leaddsub  10053  ltleadd  10060  ltaddsublt  10201  recex  10206  recp1lt1  10468  recreclt  10469  cju  10557  nnge1  10587  addltmul  10799  avglt1  10801  avglt2  10802  avgle1  10803  avgle2  10804  uzindOLD  10982  irradd  11235  rpnnen1lem5  11241  rpaddcl  11269  xaddf  11452  xaddnemnf  11462  xaddnepnf  11463  xnegdi  11469  xaddass  11470  xadddilem  11515  iooshf  11632  ge0addcl  11661  icoshft  11671  icoshftf1o  11672  iccshftr  11683  difelfznle  11818  elfzodifsumelfzo  11882  flbi2  11953  modcyc  12031  modadd1  12033  serfre  12136  sermono  12139  serge0  12161  serle  12162  bernneq  12292  faclbnd6  12377  hashfun  12495  ccatsymb  12600  swrdswrdlem  12684  swrdccatin2  12712  cshweqrep  12789  cshwcsh2id  12796  readd  12959  imadd  12967  elicc4abs  13152  rddif  13173  absrdbnd  13174  caubnd2  13190  mulcn2  13418  o1add  13436  o1sub  13438  lo1add  13449  fsumrecl  13556  efgt1  13851  pythagtriplem12  14350  pythagtriplem14  14352  pythagtriplem16  14354  remulg  18643  resubdrg  18644  prdsxmetlem  20871  xmeter  20936  bl2ioo  21297  ioo2bl  21298  ioo2blex  21299  blssioo  21300  reperf  21324  reconnlem2  21332  opnreen  21336  icopnfcnv  21442  pcoass  21524  pjthlem1  21852  ovolun  21910  shft2rab  21919  volun  21955  mbfaddlem  22067  i1fadd  22102  itg1addlem4  22106  itg2monolem1  22157  ply1divex  22537  psercnlem1  22820  reefgim  22845  tangtx  22898  efif1olem1  22929  efif1olem2  22930  efif1o  22933  relogmul  22976  argimgt0  22997  logimul  22999  ang180lem1  23141  atanlogaddlem  23244  atanlogsublem  23246  atantan  23254  ressatans  23265  emcllem6  23330  basellem9  23362  ppiub  23479  bposlem5  23563  bposlem6  23564  bposlem9  23567  chpchtlim  23664  mulog2sumlem1  23719  mulog2sumlem2  23720  selberglem2  23731  pntrmax  23749  pntpbnd1a  23770  pntpbnd2  23772  pntibndlem3  23777  pntlemb  23782  pntlemk  23791  axsegconlem7  24226  axsegconlem9  24228  axsegconlem10  24229  clwwisshclwwlem1  24805  readdsubgo  25355  pjhthlem1  26309  staddi  27165  stadd3i  27167  cdj1i  27352  cdj3lem2b  27356  cdj3i  27360  addltmulALT  27365  raddcn  27911  subfacval3  28633  rerisefaccl  29139  rprisefaccl  29145  supadd  30042  cos2h  30046  tan2h  30047  heicant  30049  mblfinlem2  30052  mblfinlem3  30053  ismblfin  30055  dvtanlem  30064  ftc1anclem3  30092  ftc1anclem4  30093  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  cntotbnd  30292  pellexlem5  30769  ioomidp  31554  stoweidlem59  31841  stirlinglem10  31865  fourierdlem103  31992  fourierdlem104  31993  fouriersw  32014  leaddsuble  32319  2leaddle2  32320  2elfz2melfz  32334  elfzelfzlble  32337  dp2cl  33163
This theorem was proved from axioms:  ax-addrcl 9574
  Copyright terms: Public domain W3C validator