Theorem readdcl 9571

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1767  (class class class)co 6282   RRcr 9487   + caddc 9491

This theorem was proved from axioms:  ax-addrcl 9549

This theorem is referenced by:  0re  9592  readdcli  9605  readdcld  9619  axltadd  9654  peano2re  9748  00id  9750  resubcl  9879  ltaddsub  10022  leaddsub  10024  ltleadd  10031  ltaddsublt  10172  recex  10177  recp1lt1  10439  recreclt  10440  cju  10528  nnge1  10558  addltmul  10770  avglt1  10772  avglt2  10773  avgle1  10774  avgle2  10775  uzindOLD  10951  irradd  11202  rpnnen1lem5  11208  rpaddcl  11236  xaddf  11419  xaddnemnf  11429  xaddnepnf  11430  xnegdi  11436  xaddass  11437  xadddilem  11482  iooshf  11599  ge0addcl  11628  icoshft  11638  icoshftf1o  11639  iccshftr  11650  difelfznle  11782  elfzodifsumelfzo  11846  flbi2  11917  modcyc  11995  modadd1  11997  serfre  12100  sermono  12103  serge0  12125  serle  12126  bernneq  12256  faclbnd6  12341  hashfun  12457  ccatsymb  12561  swrdswrdlem  12643  swrdccatin2  12671  cshweqrep  12748  cshwcsh2id  12755  readd  12918  imadd  12926  elicc4abs  13111  rddif  13132  absrdbnd  13133  caubnd2  13149  mulcn2  13377  o1add  13395  o1sub  13397  lo1add  13408  fsumrecl  13515  efgt1  13708  pythagtriplem12  14205  pythagtriplem14  14207  pythagtriplem16  14209  remulg  18410  resubdrg  18411  prdsxmetlem  20606  xmeter  20671  bl2ioo  21032  ioo2bl  21033  ioo2blex  21034  blssioo  21035  reperf  21059  reconnlem2  21067  opnreen  21071  icopnfcnv  21177  pcoass  21259  pjthlem1  21587  ovolun  21645  shft2rab  21654  volun  21690  mbfaddlem  21802  i1fadd  21837  itg1addlem4  21841  itg2monolem1  21892  ply1divex  22272  psercnlem1  22554  reefgim  22579  tangtx  22631  efif1olem1  22662  efif1olem2  22663  efif1o  22666  relogmul  22704  argimgt0  22725  logimul  22727  ang180lem1  22869  atanlogaddlem  22972  atanlogsublem  22974  atantan  22982  ressatans  22993  emcllem6  23058  basellem9  23090  ppiub  23207  bposlem5  23291  bposlem6  23292  bposlem9  23295  chpchtlim  23392  mulog2sumlem1  23447  mulog2sumlem2  23448  selberglem2  23459  pntrmax  23477  pntpbnd1a  23498  pntpbnd2  23500  pntibndlem3  23505  pntlemb  23510  pntlemk  23519  axsegconlem7  23902  axsegconlem9  23904  axsegconlem10  23905  clwwisshclwwlem1  24481  readdsubgo  25031  pjhthlem1  25985  staddi  26841  stadd3i  26843  cdj1i  27028  cdj3lem2b  27032  cdj3i  27036  addltmulALT  27041  raddcn  27547  subfacval3  28273  rerisefaccl  28716  rprisefaccl  28722  supadd  29619  cos2h  29623  tan2h  29624  heicant  29626  mblfinlem2  29629  mblfinlem3  29630  ismblfin  29632  dvtanlem  29641  ftc1anclem3  29669  ftc1anclem4  29670  ftc1anclem6  29672  ftc1anclem7  29673  ftc1anclem8  29674  cntotbnd  29895  pellexlem5  30373  zltlesub  31045  ioomidp  31118  dvbdfbdioolem2  31259  stoweidlem59  31359  stirlinglem10  31383  fourierdlem6  31413  fourierdlem10  31417  fourierdlem18  31425  fourierdlem26  31433  fourierdlem35  31442  fourierdlem50  31457  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem78  31485  fourierdlem79  31486  fourierdlem87  31494  fourierdlem103  31510  fourierdlem104  31511  fouriersw  31532  leaddsuble  31788  2leaddle2  31789  2elfz2melfz  31803  elfzelfzlble  31806  dp2cl  32244