Theorem readdcl 11113

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7360  ℝcr 11029   + caddc 11033

This theorem was proved from axioms:  ax-addrcl 11091

This theorem is referenced by:  0re  11138  readdcli  11151  readdcld  11165  axltadd  11210  peano2re  11310  00id  11312  0cnALT  11372  resubcl  11449  ltaddsub  11615  leaddsub  11617  ltleadd  11624  ltaddsublt  11768  recex  11773  recp1lt1  12044  recreclt  12045  supadd  12114  cju  12145  nnge1  12177  addltmul  12381  avglt1  12383  avglt2  12384  avgle1  12385  avgle2  12386  nzadd  12543  irradd  12890  rpnnen1lem5  12898  rpaddcl  12933  xaddf  13143  xaddnemnf  13155  xaddnepnf  13156  xnegdi  13167  xaddass  13168  xadddilem  13213  iooshf  13346  ge0addcl  13380  icoshft  13393  icoshftf1o  13394  iccshftr  13406  difelfznle  13562  elfzodifsumelfzo  13651  subfzo0  13712  flbi2  13741  modcyc  13830  modadd1  13832  modsumfzodifsn  13871  serfre  13958  sermono  13961  serge0  13983  serle  13984  bernneq  14156  faclbnd6  14226  hashfun  14364  ccatsymb  14510  swrdswrdlem  14631  swrdccatin2  14656  cshweqrep  14748  cshwcsh2id  14755  readd  15053  imadd  15061  elicc4abs  15247  rddif  15268  absrdbnd  15269  caubnd2  15285  mulcn2  15523  o1add  15541  o1sub  15543  lo1add  15554  fsumrecl  15661  rerisefaccl  15944  rprisefaccl  15950  efgt1  16045  pythagtriplem12  16758  pythagtriplem14  16760  pythagtriplem16  16762  remulg  21566  resubdrg  21567  prdsxmetlem  24316  xmeter  24381  bl2ioo  24740  ioo2bl  24741  ioo2blex  24742  blssioo  24743  reperf  24768  reconnlem2  24776  opnreen  24780  icopnfcnv  24900  pcoass  24984  pjthlem1  25397  ovolun  25460  shft2rab  25469  volun  25506  mbfaddlem  25621  i1fadd  25656  itg1addlem4  25660  itg2monolem1  25711  ply1divex  26102  psercnlem1  26395  reefgim  26420  tangtx  26474  efif1olem1  26511  efif1olem2  26512  efif1o  26515  relogmul  26561  argimgt0  26581  logimul  26583  ang180lem1  26779  atanlogaddlem  26883  atanlogsublem  26885  atantan  26893  ressatans  26904  emcllem6  26971  basellem9  27059  ppiub  27175  bposlem5  27259  bposlem6  27260  bposlem9  27263  chpchtlim  27450  mulog2sumlem1  27505  mulog2sumlem2  27506  selberglem2  27517  pntrmax  27535  pntpbnd1a  27556  pntpbnd2  27558  pntibndlem3  27563  pntlemb  27568  pntlemk  27577  axsegconlem7  28979  axsegconlem9  28981  axsegconlem10  28982  clwwisshclwwslemlem  30071  eucrctshift  30301  pjhthlem1  31449  staddi  32304  stadd3i  32306  cdj1i  32491  cdj3lem2b  32495  cdj3i  32499  addltmulALT  32504  dp2cl  32942  rpdp2cl  32944  raddcn  34067  subfacval3  35364  dnicld1  36647  dnibndlem2  36654  dnibndlem3  36655  dnibndlem5  36657  dnibndlem7  36659  iooelexlt  37538  cos2h  37783  tan2h  37784  poimir  37825  heicant  37827  mblfinlem2  37830  mblfinlem3  37831  ismblfin  37833  ftc1anclem3  37867  ftc1anclem4  37868  ftc1anclem6  37870  ftc1anclem7  37871  ftc1anclem8  37872  cntotbnd  37968  elre0re  42545  repncan2  42673  readdsub  42675  reltsubadd2  42678  resubsub4  42680  repnpcan  42683  reppncan  42684  pellexlem5  43111  ioomidp  45796  stoweidlem59  46339  stirlinglem10  46363  fourierdlem103  46489  fourierdlem104  46490  fouriersw  46511  sge0isum  46707  sge0seq  46726  hoidmvlelem2  46876  smflimlem4  47054  smfmullem1  47071  leaddsuble  47579  2leaddle2  47580  2elfz2melfz  47600  elfzelfzlble  47603  fmtnodvds  47826  gbegt5  48043  ltsubaddb  48796  ltsubadd2b  48798