Theorem readdcl 9627

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

Syntax hints:   -> wi 4   /\ wa 371   e. wcel 1889  (class class class)co 6295   RRcr 9543   + caddc 9547

This theorem was proved from axioms:  ax-addrcl 9605

This theorem is referenced by:  0re  9648  readdcli  9661  readdcld  9675  axltadd  9712  peano2re  9811  00id  9813  resubcl  9943  ltaddsub  10095  leaddsub  10097  ltleadd  10104  ltaddsublt  10246  recex  10251  recp1lt1  10511  recreclt  10512  supadd  10582  cju  10612  nnge1  10642  addltmul  10855  avglt1  10857  avglt2  10858  avgle1  10859  avgle2  10860  irradd  11295  rpnnen1lem5  11301  rpaddcl  11330  xaddf  11524  xaddnemnf  11534  xaddnepnf  11535  xnegdi  11541  xaddass  11542  xadddilem  11587  iooshf  11720  ge0addcl  11751  icoshft  11761  icoshftf1o  11762  iccshftr  11773  difelfznle  11912  elfzodifsumelfzo  11987  flbi2  12059  modcyc  12139  modadd1  12141  serfre  12249  sermono  12252  serge0  12274  serle  12275  bernneq  12405  faclbnd6  12491  hashfun  12616  ccatsymb  12734  swrdswrdlem  12822  swrdccatin2  12850  cshweqrep  12927  cshwcsh2id  12934  readd  13201  imadd  13209  elicc4abs  13394  rddif  13415  absrdbnd  13416  caubnd2  13432  mulcn2  13671  o1add  13689  o1sub  13691  lo1add  13702  fsumrecl  13812  rerisefaccl  14082  rprisefaccl  14088  efgt1  14182  pythagtriplem12  14788  pythagtriplem14  14790  pythagtriplem16  14792  remulg  19187  resubdrg  19188  prdsxmetlem  21395  xmeter  21460  bl2ioo  21822  ioo2bl  21823  ioo2blex  21824  blssioo  21825  reperf  21849  reconnlem2  21857  opnreen  21861  icopnfcnv  21982  pcoass  22067  pjthlem1  22403  ovolun  22464  shft2rab  22473  volun  22510  mbfaddlem  22628  i1fadd  22665  itg1addlem4  22669  itg2monolem1  22720  ply1divex  23099  psercnlem1  23392  reefgim  23417  tangtx  23472  efif1olem1  23503  efif1olem2  23504  efif1o  23507  relogmul  23553  argimgt0  23573  logimul  23575  ang180lem1  23750  atanlogaddlem  23851  atanlogsublem  23853  atantan  23861  ressatans  23872  emcllem6  23938  basellem9  24027  ppiub  24144  bposlem5  24228  bposlem6  24229  bposlem9  24232  chpchtlim  24329  mulog2sumlem1  24384  mulog2sumlem2  24385  selberglem2  24396  pntrmax  24414  pntpbnd1a  24435  pntpbnd2  24437  pntibndlem3  24442  pntlemb  24447  pntlemk  24456  axsegconlem7  24965  axsegconlem9  24967  axsegconlem10  24968  clwwisshclwwlem1  25545  readdsubgo  26093  pjhthlem1  27056  staddi  27911  stadd3i  27913  cdj1i  28098  cdj3lem2b  28102  cdj3i  28106  addltmulALT  28111  raddcn  28747  subfacval3  29924  iooelexlt  31777  cos2h  31948  tan2h  31949  poimir  31985  heicant  31987  mblfinlem2  31990  mblfinlem3  31991  ismblfin  31993  dvtanlemOLD  32003  ftc1anclem3  32031  ftc1anclem4  32032  ftc1anclem6  32034  ftc1anclem7  32035  ftc1anclem8  32036  cntotbnd  32140  pellexlem5  35689  ioomidp  37625  stoweidlem59  37930  stirlinglem10  37955  fourierdlem103  38083  fourierdlem104  38084  fouriersw  38105  sge0isum  38279  hoidmvlelem2  38428  gbegt5  38872  leaddsuble  39053  2leaddle2  39054  2elfz2melfz  39068  elfzelfzlble  39071  ltsubaddb  40415  ltsubadd2b  40417  dp2cl  40593