Theorem readdcl 9592

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1819  (class class class)co 6296   RRcr 9508   + caddc 9512

This theorem was proved from axioms:  ax-addrcl 9570

This theorem is referenced by:  0re  9613  readdcli  9626  readdcld  9640  axltadd  9675  peano2re  9770  00id  9772  resubcl  9902  ltaddsub  10047  leaddsub  10049  ltleadd  10056  ltaddsublt  10197  recex  10202  recp1lt1  10463  recreclt  10464  cju  10552  nnge1  10582  addltmul  10795  avglt1  10797  avglt2  10798  avgle1  10799  avgle2  10800  uzindOLD  10978  irradd  11231  rpnnen1lem5  11237  rpaddcl  11265  xaddf  11448  xaddnemnf  11458  xaddnepnf  11459  xnegdi  11465  xaddass  11466  xadddilem  11511  iooshf  11628  ge0addcl  11657  icoshft  11667  icoshftf1o  11668  iccshftr  11679  difelfznle  11814  elfzodifsumelfzo  11884  flbi2  11955  modcyc  12033  modadd1  12035  serfre  12138  sermono  12141  serge0  12163  serle  12164  bernneq  12294  faclbnd6  12379  hashfun  12498  ccatsymb  12608  swrdswrdlem  12695  swrdccatin2  12723  cshweqrep  12800  cshwcsh2id  12807  readd  12970  imadd  12978  elicc4abs  13163  rddif  13184  absrdbnd  13185  caubnd2  13201  mulcn2  13429  o1add  13447  o1sub  13449  lo1add  13460  fsumrecl  13567  efgt1  13862  pythagtriplem12  14361  pythagtriplem14  14363  pythagtriplem16  14365  remulg  18769  resubdrg  18770  prdsxmetlem  20996  xmeter  21061  bl2ioo  21422  ioo2bl  21423  ioo2blex  21424  blssioo  21425  reperf  21449  reconnlem2  21457  opnreen  21461  icopnfcnv  21567  pcoass  21649  pjthlem1  21977  ovolun  22035  shft2rab  22044  volun  22080  mbfaddlem  22192  i1fadd  22227  itg1addlem4  22231  itg2monolem1  22282  ply1divex  22662  psercnlem1  22945  reefgim  22970  tangtx  23023  efif1olem1  23054  efif1olem2  23055  efif1o  23058  relogmul  23101  argimgt0  23122  logimul  23124  ang180lem1  23266  atanlogaddlem  23369  atanlogsublem  23371  atantan  23379  ressatans  23390  emcllem6  23455  basellem9  23487  ppiub  23604  bposlem5  23688  bposlem6  23689  bposlem9  23692  chpchtlim  23789  mulog2sumlem1  23844  mulog2sumlem2  23845  selberglem2  23856  pntrmax  23874  pntpbnd1a  23895  pntpbnd2  23897  pntibndlem3  23902  pntlemb  23907  pntlemk  23916  axsegconlem7  24352  axsegconlem9  24354  axsegconlem10  24355  clwwisshclwwlem1  24931  readdsubgo  25481  pjhthlem1  26435  staddi  27291  stadd3i  27293  cdj1i  27478  cdj3lem2b  27482  cdj3i  27486  addltmulALT  27491  raddcn  28064  subfacval3  28808  rerisefaccl  29314  rprisefaccl  29320  supadd  30204  cos2h  30208  tan2h  30209  heicant  30211  mblfinlem2  30214  mblfinlem3  30215  ismblfin  30217  dvtanlem  30226  ftc1anclem3  30254  ftc1anclem4  30255  ftc1anclem6  30257  ftc1anclem7  30258  ftc1anclem8  30259  cntotbnd  30454  pellexlem5  30931  ioomidp  31715  stoweidlem59  32002  stirlinglem10  32026  fourierdlem103  32153  fourierdlem104  32154  fouriersw  32175  leaddsuble  32541  2leaddle2  32542  2elfz2melfz  32556  elfzelfzlble  32559  dp2cl  33265