Theorem readdcl 10355

Description: Alias for ax-addrcl 10333, for naming consistency with readdcli 10392. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
readdcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcl

Step	Hyp	Ref	Expression
1		ax-addrcl 10333	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107  (class class class)co 6922  ℝcr 10271   + caddc 10275

This theorem was proved from axioms:  ax-addrcl 10333

This theorem is referenced by:  0re  10378  0reOLD  10379  readdcli  10392  readdcld  10406  axltadd  10450  peano2re  10549  00id  10551  0cnALT  10610  resubcl  10687  ltaddsub  10849  leaddsub  10851  ltleadd  10858  ltaddsublt  11002  recex  11007  recp1lt1  11275  recreclt  11276  supadd  11345  cju  11370  nnge1  11404  addltmul  11618  avglt1  11620  avglt2  11621  avgle1  11622  avgle2  11623  nzadd  11777  irradd  12120  rpnnen1lem5  12128  rpaddcl  12161  xaddf  12367  xaddnemnf  12379  xaddnepnf  12380  xnegdi  12390  xaddass  12391  xadddilem  12436  iooshf  12564  ge0addcl  12598  icoshft  12609  icoshftf1o  12610  iccshftr  12623  difelfznle  12772  elfzodifsumelfzo  12853  subfzo0  12909  flbi2  12937  modcyc  13024  modadd1  13026  modsumfzodifsn  13062  serfre  13148  sermono  13151  serge0  13173  serle  13174  bernneq  13309  faclbnd6  13404  hashfun  13538  ccatsymb  13672  swrdswrdlem  13813  swrdccatin2  13856  cshweqrep  13972  cshwcsh2id  13979  readd  14273  imadd  14281  elicc4abs  14466  rddif  14487  absrdbnd  14488  caubnd2  14504  mulcn2  14734  o1add  14752  o1sub  14754  lo1add  14765  fsumrecl  14872  rerisefaccl  15150  rprisefaccl  15156  efgt1  15248  pythagtriplem12  15935  pythagtriplem14  15937  pythagtriplem16  15939  remulg  20350  resubdrg  20351  prdsxmetlem  22581  xmeter  22646  bl2ioo  23003  ioo2bl  23004  ioo2blex  23005  blssioo  23006  reperf  23030  reconnlem2  23038  opnreen  23042  icopnfcnv  23149  pcoass  23231  pjthlem1  23643  ovolun  23703  shft2rab  23712  volun  23749  mbfaddlem  23864  i1fadd  23899  itg1addlem4  23903  itg2monolem1  23954  ply1divex  24333  psercnlem1  24616  reefgim  24641  tangtx  24695  efif1olem1  24726  efif1olem2  24727  efif1o  24730  relogmul  24775  argimgt0  24795  logimul  24797  ang180lem1  24987  atanlogaddlem  25091  atanlogsublem  25093  atantan  25101  ressatans  25112  emcllem6  25179  basellem9  25267  ppiub  25381  bposlem5  25465  bposlem6  25466  bposlem9  25469  chpchtlim  25620  mulog2sumlem1  25675  mulog2sumlem2  25676  selberglem2  25687  pntrmax  25705  pntpbnd1a  25726  pntpbnd2  25728  pntibndlem3  25733  pntlemb  25738  pntlemk  25747  axsegconlem7  26272  axsegconlem9  26274  axsegconlem10  26275  clwwisshclwwslemlem  27402  eucrctshift  27647  pjhthlem1  28822  staddi  29677  stadd3i  29679  cdj1i  29864  cdj3lem2b  29868  cdj3i  29872  addltmulALT  29877  dp2cl  30150  rpdp2cl  30152  raddcn  30573  subfacval3  31770  dnicld1  33045  dnibndlem2  33052  dnibndlem3  33053  dnibndlem5  33055  dnibndlem7  33057  iooelexlt  33805  cos2h  34025  tan2h  34026  poimir  34068  heicant  34070  mblfinlem2  34073  mblfinlem3  34074  ismblfin  34076  ftc1anclem3  34112  ftc1anclem4  34113  ftc1anclem6  34115  ftc1anclem7  34116  ftc1anclem8  34117  cntotbnd  34219  elre0re  38141  repncan2  38191  readdsub  38193  resubsub4  38196  repnpcan  38199  pellexlem5  38357  ioomidp  40649  stoweidlem59  41203  stirlinglem10  41227  fourierdlem103  41353  fourierdlem104  41354  fouriersw  41375  sge0isum  41568  sge0seq  41587  hoidmvlelem2  41737  smflimlem4  41909  smfmullem1  41925  leaddsuble  42339  2leaddle2  42340  2elfz2melfz  42360  elfzelfzlble  42363  fmtnodvds  42477  gbegt5  42674  ltsubaddb  43319  ltsubadd2b  43321