Theorem readdcl 11151

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067   + caddc 11071

This theorem was proved from axioms:  ax-addrcl 11129

This theorem is referenced by:  0re  11176  readdcli  11189  readdcld  11203  axltadd  11247  peano2re  11347  00id  11349  0cnALT  11409  resubcl  11486  ltaddsub  11652  leaddsub  11654  ltleadd  11661  ltaddsublt  11805  recex  11810  recp1lt1  12081  recreclt  12082  supadd  12151  cju  12182  nnge1  12214  addltmul  12418  avglt1  12420  avglt2  12421  avgle1  12422  avgle2  12423  nzadd  12581  irradd  12932  rpnnen1lem5  12940  rpaddcl  12975  xaddf  13184  xaddnemnf  13196  xaddnepnf  13197  xnegdi  13208  xaddass  13209  xadddilem  13254  iooshf  13387  ge0addcl  13421  icoshft  13434  icoshftf1o  13435  iccshftr  13447  difelfznle  13603  elfzodifsumelfzo  13692  subfzo0  13750  flbi2  13779  modcyc  13868  modadd1  13870  modsumfzodifsn  13909  serfre  13996  sermono  13999  serge0  14021  serle  14022  bernneq  14194  faclbnd6  14264  hashfun  14402  ccatsymb  14547  swrdswrdlem  14669  swrdccatin2  14694  cshweqrep  14786  cshwcsh2id  14794  readd  15092  imadd  15100  elicc4abs  15286  rddif  15307  absrdbnd  15308  caubnd2  15324  mulcn2  15562  o1add  15580  o1sub  15582  lo1add  15593  fsumrecl  15700  rerisefaccl  15983  rprisefaccl  15989  efgt1  16084  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  remulg  21516  resubdrg  21517  prdsxmetlem  24256  xmeter  24321  bl2ioo  24680  ioo2bl  24681  ioo2blex  24682  blssioo  24683  reperf  24708  reconnlem2  24716  opnreen  24720  icopnfcnv  24840  pcoass  24924  pjthlem1  25337  ovolun  25400  shft2rab  25409  volun  25446  mbfaddlem  25561  i1fadd  25596  itg1addlem4  25600  itg2monolem1  25651  ply1divex  26042  psercnlem1  26335  reefgim  26360  tangtx  26414  efif1olem1  26451  efif1olem2  26452  efif1o  26455  relogmul  26501  argimgt0  26521  logimul  26523  ang180lem1  26719  atanlogaddlem  26823  atanlogsublem  26825  atantan  26833  ressatans  26844  emcllem6  26911  basellem9  26999  ppiub  27115  bposlem5  27199  bposlem6  27200  bposlem9  27203  chpchtlim  27390  mulog2sumlem1  27445  mulog2sumlem2  27446  selberglem2  27457  pntrmax  27475  pntpbnd1a  27496  pntpbnd2  27498  pntibndlem3  27503  pntlemb  27508  pntlemk  27517  axsegconlem7  28850  axsegconlem9  28852  axsegconlem10  28853  clwwisshclwwslemlem  29942  eucrctshift  30172  pjhthlem1  31320  staddi  32175  stadd3i  32177  cdj1i  32362  cdj3lem2b  32366  cdj3i  32370  addltmulALT  32375  dp2cl  32800  rpdp2cl  32802  raddcn  33919  subfacval3  35176  dnicld1  36460  dnibndlem2  36467  dnibndlem3  36468  dnibndlem5  36470  dnibndlem7  36472  iooelexlt  37350  cos2h  37605  tan2h  37606  poimir  37647  heicant  37649  mblfinlem2  37652  mblfinlem3  37653  ismblfin  37655  ftc1anclem3  37689  ftc1anclem4  37690  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  cntotbnd  37790  elre0re  42242  repncan2  42370  readdsub  42372  reltsubadd2  42375  resubsub4  42377  repnpcan  42380  reppncan  42381  pellexlem5  42821  ioomidp  45512  stoweidlem59  46057  stirlinglem10  46081  fourierdlem103  46207  fourierdlem104  46208  fouriersw  46229  sge0isum  46425  sge0seq  46444  hoidmvlelem2  46594  smflimlem4  46772  smfmullem1  46789  leaddsuble  47298  2leaddle2  47299  2elfz2melfz  47319  elfzelfzlble  47322  fmtnodvds  47545  gbegt5  47762  ltsubaddb  48503  ltsubadd2b  48505