Theorem readdcl 11119

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  (class class class)co 7363  ℝcr 11035   + caddc 11039

This theorem was proved from axioms:  ax-addrcl 11097

This theorem is referenced by:  0re  11144  readdcli  11158  readdcld  11172  axltadd  11217  peano2re  11317  00id  11319  0cnALT  11379  resubcl  11456  ltaddsub  11622  leaddsub  11624  ltleadd  11631  ltaddsublt  11775  recex  11780  recp1lt1  12052  recreclt  12053  supadd  12122  cju  12153  nnge1  12203  addltmul  12411  avglt1  12413  avglt2  12414  avgle1  12415  avgle2  12416  nzadd  12573  irradd  12921  rpnnen1lem5  12929  rpaddcl  12964  xaddf  13174  xaddnemnf  13186  xaddnepnf  13187  xnegdi  13198  xaddass  13199  xadddilem  13244  iooshf  13377  ge0addcl  13411  icoshft  13424  icoshftf1o  13425  iccshftr  13437  difelfznle  13594  elfzodifsumelfzo  13684  subfzo0  13745  flbi2  13774  modcyc  13863  modadd1  13865  modsumfzodifsn  13904  serfre  13991  sermono  13994  serge0  14016  serle  14017  bernneq  14189  faclbnd6  14259  hashfun  14397  ccatsymb  14543  swrdswrdlem  14664  swrdccatin2  14689  cshweqrep  14781  cshwcsh2id  14788  readd  15086  imadd  15094  elicc4abs  15280  rddif  15301  absrdbnd  15302  caubnd2  15318  mulcn2  15556  o1add  15574  o1sub  15576  lo1add  15587  fsumrecl  15694  rerisefaccl  15980  rprisefaccl  15986  efgt1  16081  pythagtriplem12  16795  pythagtriplem14  16797  pythagtriplem16  16799  remulg  21589  resubdrg  21590  prdsxmetlem  24358  xmeter  24423  bl2ioo  24782  ioo2bl  24783  ioo2blex  24784  blssioo  24785  reperf  24810  reconnlem2  24818  opnreen  24822  icopnfcnv  24934  pcoass  25016  pjthlem1  25429  ovolun  25491  shft2rab  25500  volun  25537  mbfaddlem  25652  i1fadd  25687  itg1addlem4  25691  itg2monolem1  25742  ply1divex  26127  psercnlem1  26415  reefgim  26440  tangtx  26494  efif1olem1  26531  efif1olem2  26532  efif1o  26535  relogmul  26581  argimgt0  26601  logimul  26603  ang180lem1  26798  atanlogaddlem  26902  atanlogsublem  26904  atantan  26912  ressatans  26923  emcllem6  26989  basellem9  27077  ppiub  27192  bposlem5  27276  bposlem6  27277  bposlem9  27280  chpchtlim  27467  mulog2sumlem1  27522  mulog2sumlem2  27523  selberglem2  27534  pntrmax  27552  pntpbnd1a  27573  pntpbnd2  27575  pntibndlem3  27580  pntlemb  27585  pntlemk  27594  axsegconlem7  29017  axsegconlem9  29019  axsegconlem10  29020  clwwisshclwwslemlem  30108  eucrctshift  30338  pjhthlem1  31487  staddi  32342  stadd3i  32344  cdj1i  32529  cdj3lem2b  32533  cdj3i  32537  addltmulALT  32542  dp2cl  32965  rpdp2cl  32967  raddcn  34120  subfacval3  35418  dnicld1  36779  dnibndlem2  36786  dnibndlem3  36787  dnibndlem5  36789  dnibndlem7  36791  iooelexlt  37725  cos2h  37979  tan2h  37980  poimir  38021  heicant  38023  mblfinlem2  38026  mblfinlem3  38027  ismblfin  38029  ftc1anclem3  38063  ftc1anclem4  38064  ftc1anclem6  38066  ftc1anclem7  38067  ftc1anclem8  38068  cntotbnd  38164  elre0re  42739  repncan2  42860  readdsub  42862  reltsubadd2  42865  resubsub4  42867  repnpcan  42870  reppncan  42871  pellexlem5  43279  ioomidp  45960  stoweidlem59  46503  stirlinglem10  46527  fourierdlem103  46653  fourierdlem104  46654  fouriersw  46675  sge0isum  46871  sge0seq  46890  hoidmvlelem2  47040  smflimlem4  47218  smfmullem1  47235  leaddsuble  47761  2leaddle2  47762  2elfz2melfz  47782  elfzelfzlble  47785  fmtnodvds  48023  gbegt5  48253  ltsubaddb  49006  ltsubadd2b  49008