Theorem readdcl 11255

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

Assertion

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

Proof of Theorem readdcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  (class class class)co 7408  ℝcr 11171   + caddc 11175

This proof depends on axioms:  ax-addrcl 11233

This theorem is used by:  0re  11282  readdcli  11296  readdcld  11310  axltadd  11355  peano2re  11455  00id  11457  0cnALT  11517  resubcl  11594  ltaddsub  11760  leaddsub  11762  ltleadd  11769  ltaddsublt  11913  recex  11918  recp1lt1  12185  recreclt  12186  supadd  12255  cju  12286  nnge1  12336  addltmul  12552  avglt1  12554  avglt2  12555  avgle1  12556  avgle2  12557  nzadd  12714  irradd  13071  rpnnen1lem5  13079  rpaddcl  13114  xaddf  13324  xaddnemnf  13336  xaddnepnf  13337  xnegdi  13348  xaddass  13349  xadddilem  13394  iooshf  13527  ge0addcl  13561  icoshft  13574  icoshftf1o  13575  iccshftr  13587  difelfznle  13745  elfzodifsumelfzo  13835  subfzo0  13897  flbi2  13926  modcyc  14015  modadd1  14017  modsumfzodifsn  14056  serfre  14143  sermono  14146  serge0  14168  serle  14169  bernneq  14341  faclbnd6  14411  hashfun  14550  ccatsymb  14696  swrdswrdlem  14821  swrdccatin2  14846  cshweqrep  14940  cshwcsh2id  14947  readd  15261  imadd  15269  elicc4abs  15455  rddif  15476  absrdbnd  15477  caubnd2  15493  mulcn2  15731  o1add  15749  o1sub  15751  lo1add  15762  fsumrecl  15868  rerisefaccl  16152  rprisefaccl  16158  efgt1  16252  pythagtriplem12  16966  pythagtriplem14  16968  pythagtriplem16  16970  remulg  21875  resubdrg  21876  prdsxmetlem  24649  xmeter  24714  bl2ioo  25073  ioo2bl  25074  ioo2blex  25075  blssioo  25076  reperf  25101  reconnlem2  25109  opnreen  25113  icopnfcnv  25225  pcoass  25307  pjthlem1  25720  ovolun  25782  shft2rab  25791  volun  25828  mbfaddlem  25943  i1fadd  25978  itg1addlem4  25982  itg2monolem1  26033  ply1divex  26417  psercnlem1  26716  reefgim  26741  tangtx  26798  efif1olem1  26834  efif1olem2  26835  efif1o  26838  relogmul  26884  argimgt0  26904  logimul  26906  ang180lem1  27101  atanlogaddlem  27205  atanlogsublem  27207  atantan  27215  ressatans  27226  emcllem6  27292  basellem9  27380  ppiub  27495  bposlem5  27579  bposlem6  27580  bposlem9  27583  chpchtlim  27770  mulog2sumlem1  27825  mulog2sumlem2  27826  selberglem2  27837  pntrmax  27855  pntpbnd1a  27876  pntpbnd2  27878  pntibndlem3  27883  pntlemb  27888  pntlemk  27897  axsegconlem7  29435  axsegconlem9  29437  axsegconlem10  29438  clwwisshclwwslemlem  30538  eucrctshift  30778  pjhthlem1  31927  staddi  32782  stadd3i  32784  cdj1i  32969  cdj3lem2b  32973  cdj3i  32977  addltmulALT  32982  dp2cl  33380  rpdp2cl  33382  raddcn  34495  subfacval3  35875  dnicld1  37260  dnibndlem2  37267  dnibndlem3  37268  dnibndlem5  37270  dnibndlem7  37272  iooelexlt  38205  cos2h  38454  tan2h  38455  poimir  38491  heicant  38493  mblfinlem2  38496  mblfinlem3  38497  ismblfin  38499  ftc1anclem3  38533  ftc1anclem4  38534  ftc1anclem6  38536  ftc1anclem7  38537  ftc1anclem8  38538  cntotbnd  38650  elre0re  43225  repncan2  43361  readdsub  43363  reltsubadd2  43366  resubsub4  43368  repnpcan  43371  reppncan  43372  pellexlem5  43778  ioomidp  46448  stoweidlem59  46991  stirlinglem10  47015  fourierdlem103  47141  fourierdlem104  47142  fouriersw  47163  sge0isum  47359  sge0seq  47378  hoidmvlelem2  47528  smflimlem4  47706  smfmullem1  47723  leaddsuble  48289  2leaddle2  48290  2elfz2melfz  48310  elfzelfzlble  48313  fmtnodvds  48551  gbegt5  48781  ltsubaddb  49548  ltsubadd2b  49550