Theorem readdcl 9352

Description: Alias for ax-addrcl 9330, for naming consistency with readdcli 9386. (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 9330	1 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1755  (class class class)co 6080   RRcr 9268   + caddc 9272

This theorem was proved from axioms:  ax-addrcl 9330

This theorem is referenced by:  0re  9373  readdcli  9386  readdcld  9400  axltadd  9435  peano2re  9529  00id  9531  resubcl  9660  ltaddsub  9800  leaddsub  9802  ltleadd  9809  ltaddsublt  9950  recex  9955  recp1lt1  10217  recreclt  10218  cju  10305  nnge1  10335  addltmul  10547  avglt1  10549  avglt2  10550  avgle1  10551  avgle2  10552  uzindOLD  10723  irradd  10964  rpnnen1lem5  10970  rpaddcl  10998  xaddf  11181  xaddnemnf  11191  xaddnepnf  11192  xnegdi  11198  xaddass  11199  xadddilem  11244  iooshf  11361  ge0addcl  11383  icoshft  11393  icoshftf1o  11394  iccshftr  11405  elfzodifsumelfzo  11587  flbi2  11648  modcyc  11726  modadd1  11728  serfre  11818  sermono  11821  serge0  11843  serle  11844  bernneq  11973  faclbnd6  12058  hashfun  12182  ccatsymb  12264  swrdswrdlem  12336  swrdccatin2  12361  cshweqrep  12438  readd  12598  imadd  12606  elicc4abs  12790  rddif  12811  absrdbnd  12812  caubnd2  12828  mulcn2  13056  o1add  13074  o1sub  13076  lo1add  13087  fsumrecl  13194  efgt1  13382  pythagtriplem12  13875  pythagtriplem14  13877  pythagtriplem16  13879  remulg  17878  resubdrg  17879  prdsxmetlem  19784  xmeter  19849  bl2ioo  20210  ioo2bl  20211  ioo2blex  20212  blssioo  20213  reperf  20237  reconnlem2  20245  opnreen  20249  icopnfcnv  20355  pcoass  20437  pjthlem1  20765  ovolun  20823  shft2rab  20832  volun  20867  mbfaddlem  20979  i1fadd  21014  itg1addlem4  21018  itg2monolem1  21069  ply1divex  21492  psercnlem1  21774  reefgim  21799  tangtx  21851  efif1olem1  21882  efif1olem2  21883  efif1o  21886  relogmul  21924  argimgt0  21945  logimul  21947  ang180lem1  22089  atanlogaddlem  22192  atanlogsublem  22194  atantan  22202  ressatans  22213  emcllem6  22278  basellem9  22310  ppiub  22427  bposlem5  22511  bposlem6  22512  bposlem9  22515  chpchtlim  22612  mulog2sumlem1  22667  mulog2sumlem2  22668  selberglem2  22679  pntrmax  22697  pntpbnd1a  22718  pntpbnd2  22720  pntibndlem3  22725  pntlemb  22730  pntlemk  22739  axsegconlem7  22991  axsegconlem9  22993  axsegconlem10  22994  readdsubgo  23662  pjhthlem1  24616  staddi  25472  stadd3i  25474  cdj1i  25659  cdj3lem2b  25663  cdj3i  25667  addltmulALT  25672  raddcn  26212  subfacval3  26924  rerisefaccl  27366  rprisefaccl  27372  supadd  28259  cos2h  28264  tan2h  28265  heicant  28267  mblfinlem2  28270  mblfinlem3  28271  ismblfin  28273  dvtanlem  28282  ftc1anclem3  28310  ftc1anclem4  28311  ftc1anclem6  28313  ftc1anclem7  28314  ftc1anclem8  28315  cntotbnd  28536  pellexlem5  29016  stoweidlem59  29697  stirlinglem10  29721  leaddsuble  30017  2leaddle2  30018  2elfz2melfz  30045  elfzelfzlble  30052  clwwisshclwwlem1  30312  erclwwlktr0  30322  difelfznle  30331  dp2cl  30810