Theorem readdcl 11238

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7431  ℝcr 11154   + caddc 11158

This theorem was proved from axioms:  ax-addrcl 11216

This theorem is referenced by:  0re  11263  readdcli  11276  readdcld  11290  axltadd  11334  peano2re  11434  00id  11436  0cnALT  11496  resubcl  11573  ltaddsub  11737  leaddsub  11739  ltleadd  11746  ltaddsublt  11890  recex  11895  recp1lt1  12166  recreclt  12167  supadd  12236  cju  12262  nnge1  12294  addltmul  12502  avglt1  12504  avglt2  12505  avgle1  12506  avgle2  12507  nzadd  12665  irradd  13015  rpnnen1lem5  13023  rpaddcl  13057  xaddf  13266  xaddnemnf  13278  xaddnepnf  13279  xnegdi  13290  xaddass  13291  xadddilem  13336  iooshf  13466  ge0addcl  13500  icoshft  13513  icoshftf1o  13514  iccshftr  13526  difelfznle  13682  elfzodifsumelfzo  13770  subfzo0  13828  flbi2  13857  modcyc  13946  modadd1  13948  modsumfzodifsn  13985  serfre  14072  sermono  14075  serge0  14097  serle  14098  bernneq  14268  faclbnd6  14338  hashfun  14476  ccatsymb  14620  swrdswrdlem  14742  swrdccatin2  14767  cshweqrep  14859  cshwcsh2id  14867  readd  15165  imadd  15173  elicc4abs  15358  rddif  15379  absrdbnd  15380  caubnd2  15396  mulcn2  15632  o1add  15650  o1sub  15652  lo1add  15663  fsumrecl  15770  rerisefaccl  16053  rprisefaccl  16059  efgt1  16152  pythagtriplem12  16864  pythagtriplem14  16866  pythagtriplem16  16868  remulg  21625  resubdrg  21626  prdsxmetlem  24378  xmeter  24443  bl2ioo  24813  ioo2bl  24814  ioo2blex  24815  blssioo  24816  reperf  24841  reconnlem2  24849  opnreen  24853  icopnfcnv  24973  pcoass  25057  pjthlem1  25471  ovolun  25534  shft2rab  25543  volun  25580  mbfaddlem  25695  i1fadd  25730  itg1addlem4  25734  itg2monolem1  25785  ply1divex  26176  psercnlem1  26469  reefgim  26494  tangtx  26547  efif1olem1  26584  efif1olem2  26585  efif1o  26588  relogmul  26634  argimgt0  26654  logimul  26656  ang180lem1  26852  atanlogaddlem  26956  atanlogsublem  26958  atantan  26966  ressatans  26977  emcllem6  27044  basellem9  27132  ppiub  27248  bposlem5  27332  bposlem6  27333  bposlem9  27336  chpchtlim  27523  mulog2sumlem1  27578  mulog2sumlem2  27579  selberglem2  27590  pntrmax  27608  pntpbnd1a  27629  pntpbnd2  27631  pntibndlem3  27636  pntlemb  27641  pntlemk  27650  axsegconlem7  28938  axsegconlem9  28940  axsegconlem10  28941  clwwisshclwwslemlem  30032  eucrctshift  30262  pjhthlem1  31410  staddi  32265  stadd3i  32267  cdj1i  32452  cdj3lem2b  32456  cdj3i  32460  addltmulALT  32465  dp2cl  32862  rpdp2cl  32864  raddcn  33928  subfacval3  35194  dnicld1  36473  dnibndlem2  36480  dnibndlem3  36481  dnibndlem5  36483  dnibndlem7  36485  iooelexlt  37363  cos2h  37618  tan2h  37619  poimir  37660  heicant  37662  mblfinlem2  37665  mblfinlem3  37666  ismblfin  37668  ftc1anclem3  37702  ftc1anclem4  37703  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  cntotbnd  37803  2xp3dxp2ge1d  42242  elre0re  42295  repncan2  42412  readdsub  42414  reltsubadd2  42417  resubsub4  42419  repnpcan  42422  reppncan  42423  pellexlem5  42844  ioomidp  45527  stoweidlem59  46074  stirlinglem10  46098  fourierdlem103  46224  fourierdlem104  46225  fouriersw  46246  sge0isum  46442  sge0seq  46461  hoidmvlelem2  46611  smflimlem4  46789  smfmullem1  46806  leaddsuble  47309  2leaddle2  47310  2elfz2melfz  47330  elfzelfzlble  47333  fmtnodvds  47531  gbegt5  47748  ltsubaddb  48431  ltsubadd2b  48433