Theorem readdcl 9611

Description: Alias for ax-addrcl 9589, for naming consistency with readdcli 9645. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
readdcl	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )

Proof of Theorem readdcl

Step	Hyp	Ref	Expression
1		ax-addrcl 9589	1 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1867  (class class class)co 6296   RRcr 9527   + caddc 9531

This theorem was proved from axioms:  ax-addrcl 9589

This theorem is referenced by:  0re  9632  readdcli  9645  readdcld  9659  axltadd  9696  peano2re  9795  00id  9797  resubcl  9927  ltaddsub  10077  leaddsub  10079  ltleadd  10086  ltaddsublt  10228  recex  10233  recp1lt1  10493  recreclt  10494  supadd  10564  cju  10594  nnge1  10624  addltmul  10837  avglt1  10839  avglt2  10840  avgle1  10841  avgle2  10842  irradd  11277  rpnnen1lem5  11283  rpaddcl  11312  xaddf  11506  xaddnemnf  11516  xaddnepnf  11517  xnegdi  11523  xaddass  11524  xadddilem  11569  iooshf  11702  ge0addcl  11731  icoshft  11741  icoshftf1o  11742  iccshftr  11753  difelfznle  11892  elfzodifsumelfzo  11966  flbi2  12038  modcyc  12118  modadd1  12120  serfre  12228  sermono  12231  serge0  12253  serle  12254  bernneq  12384  faclbnd6  12470  hashfun  12593  ccatsymb  12703  swrdswrdlem  12789  swrdccatin2  12817  cshweqrep  12894  cshwcsh2id  12901  readd  13157  imadd  13165  elicc4abs  13350  rddif  13371  absrdbnd  13372  caubnd2  13388  mulcn2  13626  o1add  13644  o1sub  13646  lo1add  13657  fsumrecl  13767  rerisefaccl  14037  rprisefaccl  14043  efgt1  14137  pythagtriplem12  14728  pythagtriplem14  14730  pythagtriplem16  14732  remulg  19099  resubdrg  19100  prdsxmetlem  21307  xmeter  21372  bl2ioo  21714  ioo2bl  21715  ioo2blex  21716  blssioo  21717  reperf  21741  reconnlem2  21749  opnreen  21753  icopnfcnv  21859  pcoass  21941  pjthlem1  22265  ovolun  22326  shft2rab  22335  volun  22372  mbfaddlem  22490  i1fadd  22527  itg1addlem4  22531  itg2monolem1  22582  ply1divex  22959  psercnlem1  23242  reefgim  23267  tangtx  23322  efif1olem1  23353  efif1olem2  23354  efif1o  23357  relogmul  23403  argimgt0  23423  logimul  23425  ang180lem1  23600  atanlogaddlem  23701  atanlogsublem  23703  atantan  23711  ressatans  23722  emcllem6  23788  basellem9  23875  ppiub  23992  bposlem5  24076  bposlem6  24077  bposlem9  24080  chpchtlim  24177  mulog2sumlem1  24232  mulog2sumlem2  24233  selberglem2  24244  pntrmax  24262  pntpbnd1a  24283  pntpbnd2  24285  pntibndlem3  24290  pntlemb  24295  pntlemk  24304  axsegconlem7  24796  axsegconlem9  24798  axsegconlem10  24799  clwwisshclwwlem1  25375  readdsubgo  25923  pjhthlem1  26876  staddi  27731  stadd3i  27733  cdj1i  27918  cdj3lem2b  27922  cdj3i  27926  addltmulALT  27931  raddcn  28571  subfacval3  29697  iooelexlt  31496  cos2h  31640  tan2h  31641  poimir  31677  heicant  31679  mblfinlem2  31682  mblfinlem3  31683  ismblfin  31685  dvtanlemOLD  31695  ftc1anclem3  31723  ftc1anclem4  31724  ftc1anclem6  31726  ftc1anclem7  31727  ftc1anclem8  31728  cntotbnd  31832  pellexlem5  35387  ioomidp  37204  stoweidlem59  37493  stirlinglem10  37518  fourierdlem103  37645  fourierdlem104  37646  fouriersw  37667  gbegt5  38265  leaddsuble  38405  2leaddle2  38406  2elfz2melfz  38420  elfzelfzlble  38423  ltsubaddb  39084  ltsubadd2b  39086  dp2cl  39263