Theorem readdcl 11158

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7390  ℝcr 11074   + caddc 11078

This theorem was proved from axioms:  ax-addrcl 11136

This theorem is referenced by:  0re  11183  readdcli  11196  readdcld  11210  axltadd  11254  peano2re  11354  00id  11356  0cnALT  11416  resubcl  11493  ltaddsub  11659  leaddsub  11661  ltleadd  11668  ltaddsublt  11812  recex  11817  recp1lt1  12088  recreclt  12089  supadd  12158  cju  12189  nnge1  12221  addltmul  12425  avglt1  12427  avglt2  12428  avgle1  12429  avgle2  12430  nzadd  12588  irradd  12939  rpnnen1lem5  12947  rpaddcl  12982  xaddf  13191  xaddnemnf  13203  xaddnepnf  13204  xnegdi  13215  xaddass  13216  xadddilem  13261  iooshf  13394  ge0addcl  13428  icoshft  13441  icoshftf1o  13442  iccshftr  13454  difelfznle  13610  elfzodifsumelfzo  13699  subfzo0  13757  flbi2  13786  modcyc  13875  modadd1  13877  modsumfzodifsn  13916  serfre  14003  sermono  14006  serge0  14028  serle  14029  bernneq  14201  faclbnd6  14271  hashfun  14409  ccatsymb  14554  swrdswrdlem  14676  swrdccatin2  14701  cshweqrep  14793  cshwcsh2id  14801  readd  15099  imadd  15107  elicc4abs  15293  rddif  15314  absrdbnd  15315  caubnd2  15331  mulcn2  15569  o1add  15587  o1sub  15589  lo1add  15600  fsumrecl  15707  rerisefaccl  15990  rprisefaccl  15996  efgt1  16091  pythagtriplem12  16804  pythagtriplem14  16806  pythagtriplem16  16808  remulg  21523  resubdrg  21524  prdsxmetlem  24263  xmeter  24328  bl2ioo  24687  ioo2bl  24688  ioo2blex  24689  blssioo  24690  reperf  24715  reconnlem2  24723  opnreen  24727  icopnfcnv  24847  pcoass  24931  pjthlem1  25344  ovolun  25407  shft2rab  25416  volun  25453  mbfaddlem  25568  i1fadd  25603  itg1addlem4  25607  itg2monolem1  25658  ply1divex  26049  psercnlem1  26342  reefgim  26367  tangtx  26421  efif1olem1  26458  efif1olem2  26459  efif1o  26462  relogmul  26508  argimgt0  26528  logimul  26530  ang180lem1  26726  atanlogaddlem  26830  atanlogsublem  26832  atantan  26840  ressatans  26851  emcllem6  26918  basellem9  27006  ppiub  27122  bposlem5  27206  bposlem6  27207  bposlem9  27210  chpchtlim  27397  mulog2sumlem1  27452  mulog2sumlem2  27453  selberglem2  27464  pntrmax  27482  pntpbnd1a  27503  pntpbnd2  27505  pntibndlem3  27510  pntlemb  27515  pntlemk  27524  axsegconlem7  28857  axsegconlem9  28859  axsegconlem10  28860  clwwisshclwwslemlem  29949  eucrctshift  30179  pjhthlem1  31327  staddi  32182  stadd3i  32184  cdj1i  32369  cdj3lem2b  32373  cdj3i  32377  addltmulALT  32382  dp2cl  32807  rpdp2cl  32809  raddcn  33926  subfacval3  35183  dnicld1  36467  dnibndlem2  36474  dnibndlem3  36475  dnibndlem5  36477  dnibndlem7  36479  iooelexlt  37357  cos2h  37612  tan2h  37613  poimir  37654  heicant  37656  mblfinlem2  37659  mblfinlem3  37660  ismblfin  37662  ftc1anclem3  37696  ftc1anclem4  37697  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  cntotbnd  37797  elre0re  42249  repncan2  42377  readdsub  42379  reltsubadd2  42382  resubsub4  42384  repnpcan  42387  reppncan  42388  pellexlem5  42828  ioomidp  45519  stoweidlem59  46064  stirlinglem10  46088  fourierdlem103  46214  fourierdlem104  46215  fouriersw  46236  sge0isum  46432  sge0seq  46451  hoidmvlelem2  46601  smflimlem4  46779  smfmullem1  46796  leaddsuble  47302  2leaddle2  47303  2elfz2melfz  47323  elfzelfzlble  47326  fmtnodvds  47549  gbegt5  47766  ltsubaddb  48507  ltsubadd2b  48509