Theorem readdcl 10623

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113  (class class class)co 7159  ℝcr 10539   + caddc 10543

This theorem was proved from axioms:  ax-addrcl 10601

This theorem is referenced by:  0re  10646  readdcli  10659  readdcld  10673  axltadd  10717  peano2re  10816  00id  10818  0cnALT  10877  resubcl  10953  ltaddsub  11117  leaddsub  11119  ltleadd  11126  ltaddsublt  11270  recex  11275  recp1lt1  11541  recreclt  11542  supadd  11612  cju  11637  nnge1  11668  addltmul  11876  avglt1  11878  avglt2  11879  avgle1  11880  avgle2  11881  nzadd  12033  irradd  12375  rpnnen1lem5  12383  rpaddcl  12414  xaddf  12620  xaddnemnf  12632  xaddnepnf  12633  xnegdi  12644  xaddass  12645  xadddilem  12690  iooshf  12818  ge0addcl  12851  icoshft  12862  icoshftf1o  12863  iccshftr  12875  difelfznle  13024  elfzodifsumelfzo  13106  subfzo0  13162  flbi2  13190  modcyc  13277  modadd1  13279  modsumfzodifsn  13315  serfre  13402  sermono  13405  serge0  13427  serle  13428  bernneq  13593  faclbnd6  13662  hashfun  13801  ccatsymb  13939  swrdswrdlem  14069  swrdccatin2  14094  cshweqrep  14186  cshwcsh2id  14193  readd  14488  imadd  14496  elicc4abs  14682  rddif  14703  absrdbnd  14704  caubnd2  14720  mulcn2  14955  o1add  14973  o1sub  14975  lo1add  14986  fsumrecl  15094  rerisefaccl  15374  rprisefaccl  15380  efgt1  15472  pythagtriplem12  16166  pythagtriplem14  16168  pythagtriplem16  16170  remulg  20754  resubdrg  20755  prdsxmetlem  22981  xmeter  23046  bl2ioo  23403  ioo2bl  23404  ioo2blex  23405  blssioo  23406  reperf  23430  reconnlem2  23438  opnreen  23442  icopnfcnv  23549  pcoass  23631  pjthlem1  24043  ovolun  24103  shft2rab  24112  volun  24149  mbfaddlem  24264  i1fadd  24299  itg1addlem4  24303  itg2monolem1  24354  ply1divex  24733  psercnlem1  25016  reefgim  25041  tangtx  25094  efif1olem1  25129  efif1olem2  25130  efif1o  25133  relogmul  25178  argimgt0  25198  logimul  25200  ang180lem1  25390  atanlogaddlem  25494  atanlogsublem  25496  atantan  25504  ressatans  25515  emcllem6  25581  basellem9  25669  ppiub  25783  bposlem5  25867  bposlem6  25868  bposlem9  25871  chpchtlim  26058  mulog2sumlem1  26113  mulog2sumlem2  26114  selberglem2  26125  pntrmax  26143  pntpbnd1a  26164  pntpbnd2  26166  pntibndlem3  26171  pntlemb  26176  pntlemk  26185  axsegconlem7  26712  axsegconlem9  26714  axsegconlem10  26715  clwwisshclwwslemlem  27794  eucrctshift  28025  pjhthlem1  29171  staddi  30026  stadd3i  30028  cdj1i  30213  cdj3lem2b  30217  cdj3i  30221  addltmulALT  30226  dp2cl  30560  rpdp2cl  30562  raddcn  31176  subfacval3  32440  dnicld1  33815  dnibndlem2  33822  dnibndlem3  33823  dnibndlem5  33825  dnibndlem7  33827  iooelexlt  34647  cos2h  34887  tan2h  34888  poimir  34929  heicant  34931  mblfinlem2  34934  mblfinlem3  34935  ismblfin  34937  ftc1anclem3  34973  ftc1anclem4  34974  ftc1anclem6  34976  ftc1anclem7  34977  ftc1anclem8  34978  cntotbnd  35078  elre0re  39160  repncan2  39218  readdsub  39220  reltsubadd2  39223  resubsub4  39225  repnpcan  39228  reppncan  39229  pellexlem5  39436  ioomidp  41796  stoweidlem59  42351  stirlinglem10  42375  fourierdlem103  42501  fourierdlem104  42502  fouriersw  42523  sge0isum  42716  sge0seq  42735  hoidmvlelem2  42885  smflimlem4  43057  smfmullem1  43073  leaddsuble  43504  2leaddle2  43505  2elfz2melfz  43525  elfzelfzlble  43528  fmtnodvds  43713  gbegt5  43933  ltsubaddb  44576  ltsubadd2b  44578