Theorem readdcl 9370

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1756  (class class class)co 6096   RRcr 9286   + caddc 9290

This theorem was proved from axioms:  ax-addrcl 9348

This theorem is referenced by:  0re  9391  readdcli  9404  readdcld  9418  axltadd  9453  peano2re  9547  00id  9549  resubcl  9678  ltaddsub  9818  leaddsub  9820  ltleadd  9827  ltaddsublt  9968  recex  9973  recp1lt1  10235  recreclt  10236  cju  10323  nnge1  10353  addltmul  10565  avglt1  10567  avglt2  10568  avgle1  10569  avgle2  10570  uzindOLD  10741  irradd  10982  rpnnen1lem5  10988  rpaddcl  11016  xaddf  11199  xaddnemnf  11209  xaddnepnf  11210  xnegdi  11216  xaddass  11217  xadddilem  11262  iooshf  11379  ge0addcl  11402  icoshft  11412  icoshftf1o  11413  iccshftr  11424  elfzodifsumelfzo  11609  flbi2  11670  modcyc  11748  modadd1  11750  serfre  11840  sermono  11843  serge0  11865  serle  11866  bernneq  11995  faclbnd6  12080  hashfun  12204  ccatsymb  12286  swrdswrdlem  12358  swrdccatin2  12383  cshweqrep  12460  readd  12620  imadd  12628  elicc4abs  12812  rddif  12833  absrdbnd  12834  caubnd2  12850  mulcn2  13078  o1add  13096  o1sub  13098  lo1add  13109  fsumrecl  13216  efgt1  13405  pythagtriplem12  13898  pythagtriplem14  13900  pythagtriplem16  13902  remulg  18042  resubdrg  18043  prdsxmetlem  19948  xmeter  20013  bl2ioo  20374  ioo2bl  20375  ioo2blex  20376  blssioo  20377  reperf  20401  reconnlem2  20409  opnreen  20413  icopnfcnv  20519  pcoass  20601  pjthlem1  20929  ovolun  20987  shft2rab  20996  volun  21031  mbfaddlem  21143  i1fadd  21178  itg1addlem4  21182  itg2monolem1  21233  ply1divex  21613  psercnlem1  21895  reefgim  21920  tangtx  21972  efif1olem1  22003  efif1olem2  22004  efif1o  22007  relogmul  22045  argimgt0  22066  logimul  22068  ang180lem1  22210  atanlogaddlem  22313  atanlogsublem  22315  atantan  22323  ressatans  22334  emcllem6  22399  basellem9  22431  ppiub  22548  bposlem5  22632  bposlem6  22633  bposlem9  22636  chpchtlim  22733  mulog2sumlem1  22788  mulog2sumlem2  22789  selberglem2  22800  pntrmax  22818  pntpbnd1a  22839  pntpbnd2  22841  pntibndlem3  22846  pntlemb  22851  pntlemk  22860  axsegconlem7  23174  axsegconlem9  23176  axsegconlem10  23177  readdsubgo  23845  pjhthlem1  24799  staddi  25655  stadd3i  25657  cdj1i  25842  cdj3lem2b  25846  cdj3i  25850  addltmulALT  25855  raddcn  26364  subfacval3  27082  rerisefaccl  27525  rprisefaccl  27531  supadd  28423  cos2h  28428  tan2h  28429  heicant  28431  mblfinlem2  28434  mblfinlem3  28435  ismblfin  28437  dvtanlem  28446  ftc1anclem3  28474  ftc1anclem4  28475  ftc1anclem6  28477  ftc1anclem7  28478  ftc1anclem8  28479  cntotbnd  28700  pellexlem5  29179  stoweidlem59  29859  stirlinglem10  29883  leaddsuble  30179  2leaddle2  30180  2elfz2melfz  30207  elfzelfzlble  30214  clwwisshclwwlem1  30474  erclwwlktr0  30484  difelfznle  30493  dp2cl  31109