Theorem readdcl 11196

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  (class class class)co 7412  ℝcr 11112   + caddc 11116

This theorem was proved from axioms:  ax-addrcl 11174

This theorem is referenced by:  0re  11221  readdcli  11234  readdcld  11248  axltadd  11292  peano2re  11392  00id  11394  0cnALT  11453  resubcl  11529  ltaddsub  11693  leaddsub  11695  ltleadd  11702  ltaddsublt  11846  recex  11851  recp1lt1  12117  recreclt  12118  supadd  12187  cju  12213  nnge1  12245  addltmul  12453  avglt1  12455  avglt2  12456  avgle1  12457  avgle2  12458  nzadd  12615  irradd  12962  rpnnen1lem5  12970  rpaddcl  13001  xaddf  13208  xaddnemnf  13220  xaddnepnf  13221  xnegdi  13232  xaddass  13233  xadddilem  13278  iooshf  13408  ge0addcl  13442  icoshft  13455  icoshftf1o  13456  iccshftr  13468  difelfznle  13620  elfzodifsumelfzo  13703  subfzo0  13759  flbi2  13787  modcyc  13876  modadd1  13878  modsumfzodifsn  13914  serfre  14002  sermono  14005  serge0  14027  serle  14028  bernneq  14197  faclbnd6  14264  hashfun  14402  ccatsymb  14537  swrdswrdlem  14659  swrdccatin2  14684  cshweqrep  14776  cshwcsh2id  14784  readd  15078  imadd  15086  elicc4abs  15271  rddif  15292  absrdbnd  15293  caubnd2  15309  mulcn2  15545  o1add  15563  o1sub  15565  lo1add  15576  fsumrecl  15685  rerisefaccl  15966  rprisefaccl  15972  efgt1  16064  pythagtriplem12  16764  pythagtriplem14  16766  pythagtriplem16  16768  remulg  21380  resubdrg  21381  prdsxmetlem  24095  xmeter  24160  bl2ioo  24529  ioo2bl  24530  ioo2blex  24531  blssioo  24532  reperf  24556  reconnlem2  24564  opnreen  24568  icopnfcnv  24688  pcoass  24772  pjthlem1  25186  ovolun  25249  shft2rab  25258  volun  25295  mbfaddlem  25410  i1fadd  25445  itg1addlem4  25449  itg1addlem4OLD  25450  itg2monolem1  25501  ply1divex  25890  psercnlem1  26174  reefgim  26199  tangtx  26252  efif1olem1  26288  efif1olem2  26289  efif1o  26292  relogmul  26337  argimgt0  26357  logimul  26359  ang180lem1  26551  atanlogaddlem  26655  atanlogsublem  26657  atantan  26665  ressatans  26676  emcllem6  26742  basellem9  26830  ppiub  26944  bposlem5  27028  bposlem6  27029  bposlem9  27032  chpchtlim  27219  mulog2sumlem1  27274  mulog2sumlem2  27275  selberglem2  27286  pntrmax  27304  pntpbnd1a  27325  pntpbnd2  27327  pntibndlem3  27332  pntlemb  27337  pntlemk  27346  axsegconlem7  28449  axsegconlem9  28451  axsegconlem10  28452  clwwisshclwwslemlem  29534  eucrctshift  29764  pjhthlem1  30912  staddi  31767  stadd3i  31769  cdj1i  31954  cdj3lem2b  31958  cdj3i  31962  addltmulALT  31967  dp2cl  32314  rpdp2cl  32316  raddcn  33208  subfacval3  34479  dnicld1  35652  dnibndlem2  35659  dnibndlem3  35660  dnibndlem5  35662  dnibndlem7  35664  iooelexlt  36547  cos2h  36783  tan2h  36784  poimir  36825  heicant  36827  mblfinlem2  36830  mblfinlem3  36831  ismblfin  36833  ftc1anclem3  36867  ftc1anclem4  36868  ftc1anclem6  36870  ftc1anclem7  36871  ftc1anclem8  36872  cntotbnd  36968  2xp3dxp2ge1d  41329  elre0re  41478  repncan2  41558  readdsub  41560  reltsubadd2  41563  resubsub4  41565  repnpcan  41568  reppncan  41569  pellexlem5  41874  ioomidp  44526  stoweidlem59  45074  stirlinglem10  45098  fourierdlem103  45224  fourierdlem104  45225  fouriersw  45246  sge0isum  45442  sge0seq  45461  hoidmvlelem2  45611  smflimlem4  45789  smfmullem1  45806  leaddsuble  46304  2leaddle2  46305  2elfz2melfz  46325  elfzelfzlble  46328  fmtnodvds  46511  gbegt5  46728  ltsubaddb  47283  ltsubadd2b  47285