Theorem readdcl 11210

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7403  ℝcr 11126   + caddc 11130

This theorem was proved from axioms:  ax-addrcl 11188

This theorem is referenced by:  0re  11235  readdcli  11248  readdcld  11262  axltadd  11306  peano2re  11406  00id  11408  0cnALT  11468  resubcl  11545  ltaddsub  11709  leaddsub  11711  ltleadd  11718  ltaddsublt  11862  recex  11867  recp1lt1  12138  recreclt  12139  supadd  12208  cju  12234  nnge1  12266  addltmul  12475  avglt1  12477  avglt2  12478  avgle1  12479  avgle2  12480  nzadd  12638  irradd  12987  rpnnen1lem5  12995  rpaddcl  13029  xaddf  13238  xaddnemnf  13250  xaddnepnf  13251  xnegdi  13262  xaddass  13263  xadddilem  13308  iooshf  13441  ge0addcl  13475  icoshft  13488  icoshftf1o  13489  iccshftr  13501  difelfznle  13657  elfzodifsumelfzo  13745  subfzo0  13803  flbi2  13832  modcyc  13921  modadd1  13923  modsumfzodifsn  13960  serfre  14047  sermono  14050  serge0  14072  serle  14073  bernneq  14245  faclbnd6  14315  hashfun  14453  ccatsymb  14598  swrdswrdlem  14720  swrdccatin2  14745  cshweqrep  14837  cshwcsh2id  14845  readd  15143  imadd  15151  elicc4abs  15336  rddif  15357  absrdbnd  15358  caubnd2  15374  mulcn2  15610  o1add  15628  o1sub  15630  lo1add  15641  fsumrecl  15748  rerisefaccl  16031  rprisefaccl  16037  efgt1  16132  pythagtriplem12  16844  pythagtriplem14  16846  pythagtriplem16  16848  remulg  21565  resubdrg  21566  prdsxmetlem  24305  xmeter  24370  bl2ioo  24729  ioo2bl  24730  ioo2blex  24731  blssioo  24732  reperf  24757  reconnlem2  24765  opnreen  24769  icopnfcnv  24889  pcoass  24973  pjthlem1  25387  ovolun  25450  shft2rab  25459  volun  25496  mbfaddlem  25611  i1fadd  25646  itg1addlem4  25650  itg2monolem1  25701  ply1divex  26092  psercnlem1  26385  reefgim  26410  tangtx  26464  efif1olem1  26501  efif1olem2  26502  efif1o  26505  relogmul  26551  argimgt0  26571  logimul  26573  ang180lem1  26769  atanlogaddlem  26873  atanlogsublem  26875  atantan  26883  ressatans  26894  emcllem6  26961  basellem9  27049  ppiub  27165  bposlem5  27249  bposlem6  27250  bposlem9  27253  chpchtlim  27440  mulog2sumlem1  27495  mulog2sumlem2  27496  selberglem2  27507  pntrmax  27525  pntpbnd1a  27546  pntpbnd2  27548  pntibndlem3  27553  pntlemb  27558  pntlemk  27567  axsegconlem7  28848  axsegconlem9  28850  axsegconlem10  28851  clwwisshclwwslemlem  29940  eucrctshift  30170  pjhthlem1  31318  staddi  32173  stadd3i  32175  cdj1i  32360  cdj3lem2b  32364  cdj3i  32368  addltmulALT  32373  dp2cl  32800  rpdp2cl  32802  raddcn  33906  subfacval3  35157  dnicld1  36436  dnibndlem2  36443  dnibndlem3  36444  dnibndlem5  36446  dnibndlem7  36448  iooelexlt  37326  cos2h  37581  tan2h  37582  poimir  37623  heicant  37625  mblfinlem2  37628  mblfinlem3  37629  ismblfin  37631  ftc1anclem3  37665  ftc1anclem4  37666  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  cntotbnd  37766  2xp3dxp2ge1d  42200  elre0re  42252  repncan2  42372  readdsub  42374  reltsubadd2  42377  resubsub4  42379  repnpcan  42382  reppncan  42383  pellexlem5  42803  ioomidp  45491  stoweidlem59  46036  stirlinglem10  46060  fourierdlem103  46186  fourierdlem104  46187  fouriersw  46208  sge0isum  46404  sge0seq  46423  hoidmvlelem2  46573  smflimlem4  46751  smfmullem1  46768  leaddsuble  47274  2leaddle2  47275  2elfz2melfz  47295  elfzelfzlble  47298  fmtnodvds  47506  gbegt5  47723  ltsubaddb  48438  ltsubadd2b  48440