Theorem readdcl 11199

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

Assertion

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

Proof of Theorem readdcl

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

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

This theorem was proved from axioms:  ax-addrcl 11177

This theorem is referenced by:  0re  11223  readdcli  11236  readdcld  11250  axltadd  11294  peano2re  11394  00id  11396  0cnALT  11455  resubcl  11531  ltaddsub  11695  leaddsub  11697  ltleadd  11704  ltaddsublt  11848  recex  11853  recp1lt1  12119  recreclt  12120  supadd  12189  cju  12215  nnge1  12247  addltmul  12455  avglt1  12457  avglt2  12458  avgle1  12459  avgle2  12460  nzadd  12617  irradd  12964  rpnnen1lem5  12972  rpaddcl  13003  xaddf  13210  xaddnemnf  13222  xaddnepnf  13223  xnegdi  13234  xaddass  13235  xadddilem  13280  iooshf  13410  ge0addcl  13444  icoshft  13457  icoshftf1o  13458  iccshftr  13470  difelfznle  13622  elfzodifsumelfzo  13705  subfzo0  13761  flbi2  13789  modcyc  13878  modadd1  13880  modsumfzodifsn  13916  serfre  14004  sermono  14007  serge0  14029  serle  14030  bernneq  14199  faclbnd6  14266  hashfun  14404  ccatsymb  14539  swrdswrdlem  14661  swrdccatin2  14686  cshweqrep  14778  cshwcsh2id  14786  readd  15080  imadd  15088  elicc4abs  15273  rddif  15294  absrdbnd  15295  caubnd2  15311  mulcn2  15547  o1add  15565  o1sub  15567  lo1add  15578  fsumrecl  15687  rerisefaccl  15968  rprisefaccl  15974  efgt1  16066  pythagtriplem12  16766  pythagtriplem14  16768  pythagtriplem16  16770  remulg  21469  resubdrg  21470  prdsxmetlem  24193  xmeter  24258  bl2ioo  24627  ioo2bl  24628  ioo2blex  24629  blssioo  24630  reperf  24654  reconnlem2  24662  opnreen  24666  icopnfcnv  24786  pcoass  24870  pjthlem1  25284  ovolun  25347  shft2rab  25356  volun  25393  mbfaddlem  25508  i1fadd  25543  itg1addlem4  25547  itg1addlem4OLD  25548  itg2monolem1  25599  ply1divex  25991  psercnlem1  26276  reefgim  26301  tangtx  26354  efif1olem1  26390  efif1olem2  26391  efif1o  26394  relogmul  26439  argimgt0  26459  logimul  26461  ang180lem1  26654  atanlogaddlem  26758  atanlogsublem  26760  atantan  26768  ressatans  26779  emcllem6  26845  basellem9  26933  ppiub  27049  bposlem5  27133  bposlem6  27134  bposlem9  27137  chpchtlim  27324  mulog2sumlem1  27379  mulog2sumlem2  27380  selberglem2  27391  pntrmax  27409  pntpbnd1a  27430  pntpbnd2  27432  pntibndlem3  27437  pntlemb  27442  pntlemk  27451  axsegconlem7  28613  axsegconlem9  28615  axsegconlem10  28616  clwwisshclwwslemlem  29698  eucrctshift  29928  pjhthlem1  31076  staddi  31931  stadd3i  31933  cdj1i  32118  cdj3lem2b  32122  cdj3i  32126  addltmulALT  32131  dp2cl  32478  rpdp2cl  32480  raddcn  33372  subfacval3  34643  dnicld1  35811  dnibndlem2  35818  dnibndlem3  35819  dnibndlem5  35821  dnibndlem7  35823  iooelexlt  36706  cos2h  36942  tan2h  36943  poimir  36984  heicant  36986  mblfinlem2  36989  mblfinlem3  36990  ismblfin  36992  ftc1anclem3  37026  ftc1anclem4  37027  ftc1anclem6  37029  ftc1anclem7  37030  ftc1anclem8  37031  cntotbnd  37127  2xp3dxp2ge1d  41488  elre0re  41637  repncan2  41717  readdsub  41719  reltsubadd2  41722  resubsub4  41724  repnpcan  41727  reppncan  41728  pellexlem5  42033  ioomidp  44685  stoweidlem59  45233  stirlinglem10  45257  fourierdlem103  45383  fourierdlem104  45384  fouriersw  45405  sge0isum  45601  sge0seq  45620  hoidmvlelem2  45770  smflimlem4  45948  smfmullem1  45965  leaddsuble  46463  2leaddle2  46464  2elfz2melfz  46484  elfzelfzlble  46487  fmtnodvds  46670  gbegt5  46887  ltsubaddb  47356  ltsubadd2b  47358