Theorem readdcl 10019

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

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990  (class class class)co 6650   RRcr 9935   + caddc 9939

This theorem was proved from axioms:  ax-addrcl 9997

This theorem is referenced by:  0re  10040  readdcli  10053  readdcld  10069  axltadd  10111  peano2re  10209  00id  10211  resubcl  10345  ltaddsub  10502  leaddsub  10504  ltleadd  10511  ltaddsublt  10654  recex  10659  recp1lt1  10921  recreclt  10922  supadd  10991  cju  11016  nnge1  11046  addltmul  11268  avglt1  11270  avglt2  11271  avgle1  11272  avgle2  11273  nzadd  11425  irradd  11812  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  rpaddcl  11854  xaddf  12055  xaddnemnf  12067  xaddnepnf  12068  xnegdi  12078  xaddass  12079  xadddilem  12124  iooshf  12252  ge0addcl  12284  icoshft  12294  icoshftf1o  12295  iccshftr  12306  difelfznle  12453  elfzodifsumelfzo  12533  subfzo0  12590  flbi2  12618  modcyc  12705  modadd1  12707  modsumfzodifsn  12743  serfre  12830  sermono  12833  serge0  12855  serle  12856  bernneq  12990  faclbnd6  13086  hashfun  13224  ccatsymb  13366  swrdswrdlem  13459  swrdccatin2  13487  cshweqrep  13567  cshwcsh2id  13574  readd  13866  imadd  13874  elicc4abs  14059  rddif  14080  absrdbnd  14081  caubnd2  14097  mulcn2  14326  o1add  14344  o1sub  14346  lo1add  14357  fsumrecl  14465  rerisefaccl  14748  rprisefaccl  14754  efgt1  14846  pythagtriplem12  15531  pythagtriplem14  15533  pythagtriplem16  15535  remulg  19953  resubdrg  19954  prdsxmetlem  22173  xmeter  22238  bl2ioo  22595  ioo2bl  22596  ioo2blex  22597  blssioo  22598  reperf  22622  reconnlem2  22630  opnreen  22634  icopnfcnv  22741  pcoass  22824  pjthlem1  23208  ovolun  23267  shft2rab  23276  volun  23313  mbfaddlem  23427  i1fadd  23462  itg1addlem4  23466  itg2monolem1  23517  ply1divex  23896  psercnlem1  24179  reefgim  24204  tangtx  24257  efif1olem1  24288  efif1olem2  24289  efif1o  24292  relogmul  24338  argimgt0  24358  logimul  24360  ang180lem1  24539  atanlogaddlem  24640  atanlogsublem  24642  atantan  24650  ressatans  24661  emcllem6  24727  basellem9  24815  ppiub  24929  bposlem5  25013  bposlem6  25014  bposlem9  25017  chpchtlim  25168  mulog2sumlem1  25223  mulog2sumlem2  25224  selberglem2  25235  pntrmax  25253  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem3  25281  pntlemb  25286  pntlemk  25295  axsegconlem7  25803  axsegconlem9  25805  axsegconlem10  25806  clwwisshclwwslemlem  26926  eucrctshift  27103  pjhthlem1  28250  staddi  29105  stadd3i  29107  cdj1i  29292  cdj3lem2b  29296  cdj3i  29300  addltmulALT  29305  dp2cl  29587  rpdp2cl  29589  raddcn  29975  subfacval3  31171  dnicld1  32462  dnibndlem2  32469  dnibndlem3  32470  dnibndlem5  32472  dnibndlem7  32474  iooelexlt  33210  cos2h  33400  tan2h  33401  poimir  33442  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  ismblfin  33450  ftc1anclem3  33487  ftc1anclem4  33488  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  cntotbnd  33595  pellexlem5  37397  ioomidp  39740  stoweidlem59  40276  stirlinglem10  40300  fourierdlem103  40426  fourierdlem104  40427  fouriersw  40448  sge0isum  40644  sge0seq  40663  hoidmvlelem2  40810  smflimlem4  40982  smfmullem1  40998  leaddsuble  41311  2leaddle2  41312  2elfz2melfz  41328  elfzelfzlble  41331  fmtnodvds  41456  gbegt5  41649  ltsubaddb  42304  ltsubadd2b  42306