Theorem readdcl 11195

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  (class class class)co 7411  ℝcr 11111   + caddc 11115

This theorem was proved from axioms:  ax-addrcl 11173

This theorem is referenced by:  0re  11220  readdcli  11233  readdcld  11247  axltadd  11291  peano2re  11391  00id  11393  0cnALT  11452  resubcl  11528  ltaddsub  11692  leaddsub  11694  ltleadd  11701  ltaddsublt  11845  recex  11850  recp1lt1  12116  recreclt  12117  supadd  12186  cju  12212  nnge1  12244  addltmul  12452  avglt1  12454  avglt2  12455  avgle1  12456  avgle2  12457  nzadd  12614  irradd  12961  rpnnen1lem5  12969  rpaddcl  13000  xaddf  13207  xaddnemnf  13219  xaddnepnf  13220  xnegdi  13231  xaddass  13232  xadddilem  13277  iooshf  13407  ge0addcl  13441  icoshft  13454  icoshftf1o  13455  iccshftr  13467  difelfznle  13619  elfzodifsumelfzo  13702  subfzo0  13758  flbi2  13786  modcyc  13875  modadd1  13877  modsumfzodifsn  13913  serfre  14001  sermono  14004  serge0  14026  serle  14027  bernneq  14196  faclbnd6  14263  hashfun  14401  ccatsymb  14536  swrdswrdlem  14658  swrdccatin2  14683  cshweqrep  14775  cshwcsh2id  14783  readd  15077  imadd  15085  elicc4abs  15270  rddif  15291  absrdbnd  15292  caubnd2  15308  mulcn2  15544  o1add  15562  o1sub  15564  lo1add  15575  fsumrecl  15684  rerisefaccl  15965  rprisefaccl  15971  efgt1  16063  pythagtriplem12  16763  pythagtriplem14  16765  pythagtriplem16  16767  remulg  21379  resubdrg  21380  prdsxmetlem  24094  xmeter  24159  bl2ioo  24528  ioo2bl  24529  ioo2blex  24530  blssioo  24531  reperf  24555  reconnlem2  24563  opnreen  24567  icopnfcnv  24687  pcoass  24771  pjthlem1  25185  ovolun  25248  shft2rab  25257  volun  25294  mbfaddlem  25409  i1fadd  25444  itg1addlem4  25448  itg1addlem4OLD  25449  itg2monolem1  25500  ply1divex  25889  psercnlem1  26173  reefgim  26198  tangtx  26251  efif1olem1  26287  efif1olem2  26288  efif1o  26291  relogmul  26336  argimgt0  26356  logimul  26358  ang180lem1  26550  atanlogaddlem  26654  atanlogsublem  26656  atantan  26664  ressatans  26675  emcllem6  26741  basellem9  26829  ppiub  26943  bposlem5  27027  bposlem6  27028  bposlem9  27031  chpchtlim  27218  mulog2sumlem1  27273  mulog2sumlem2  27274  selberglem2  27285  pntrmax  27303  pntpbnd1a  27324  pntpbnd2  27326  pntibndlem3  27331  pntlemb  27336  pntlemk  27345  axsegconlem7  28448  axsegconlem9  28450  axsegconlem10  28451  clwwisshclwwslemlem  29533  eucrctshift  29763  pjhthlem1  30911  staddi  31766  stadd3i  31768  cdj1i  31953  cdj3lem2b  31957  cdj3i  31961  addltmulALT  31966  dp2cl  32313  rpdp2cl  32315  raddcn  33207  subfacval3  34478  dnicld1  35651  dnibndlem2  35658  dnibndlem3  35659  dnibndlem5  35661  dnibndlem7  35663  iooelexlt  36546  cos2h  36782  tan2h  36783  poimir  36824  heicant  36826  mblfinlem2  36829  mblfinlem3  36830  ismblfin  36832  ftc1anclem3  36866  ftc1anclem4  36867  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  cntotbnd  36967  2xp3dxp2ge1d  41328  elre0re  41477  repncan2  41557  readdsub  41559  reltsubadd2  41562  resubsub4  41564  repnpcan  41567  reppncan  41568  pellexlem5  41873  ioomidp  44525  stoweidlem59  45073  stirlinglem10  45097  fourierdlem103  45223  fourierdlem104  45224  fouriersw  45245  sge0isum  45441  sge0seq  45460  hoidmvlelem2  45610  smflimlem4  45788  smfmullem1  45805  leaddsuble  46303  2leaddle2  46304  2elfz2melfz  46324  elfzelfzlble  46327  fmtnodvds  46510  gbegt5  46727  ltsubaddb  47282  ltsubadd2b  47284