Theorem readdcl 11081

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2110  (class class class)co 7341  ℝcr 10997   + caddc 11001

This theorem was proved from axioms:  ax-addrcl 11059

This theorem is referenced by:  0re  11106  readdcli  11119  readdcld  11133  axltadd  11178  peano2re  11278  00id  11280  0cnALT  11340  resubcl  11417  ltaddsub  11583  leaddsub  11585  ltleadd  11592  ltaddsublt  11736  recex  11741  recp1lt1  12012  recreclt  12013  supadd  12082  cju  12113  nnge1  12145  addltmul  12349  avglt1  12351  avglt2  12352  avgle1  12353  avgle2  12354  nzadd  12512  irradd  12863  rpnnen1lem5  12871  rpaddcl  12906  xaddf  13115  xaddnemnf  13127  xaddnepnf  13128  xnegdi  13139  xaddass  13140  xadddilem  13185  iooshf  13318  ge0addcl  13352  icoshft  13365  icoshftf1o  13366  iccshftr  13378  difelfznle  13534  elfzodifsumelfzo  13623  subfzo0  13684  flbi2  13713  modcyc  13802  modadd1  13804  modsumfzodifsn  13843  serfre  13930  sermono  13933  serge0  13955  serle  13956  bernneq  14128  faclbnd6  14198  hashfun  14336  ccatsymb  14482  swrdswrdlem  14603  swrdccatin2  14628  cshweqrep  14720  cshwcsh2id  14727  readd  15025  imadd  15033  elicc4abs  15219  rddif  15240  absrdbnd  15241  caubnd2  15257  mulcn2  15495  o1add  15513  o1sub  15515  lo1add  15526  fsumrecl  15633  rerisefaccl  15916  rprisefaccl  15922  efgt1  16017  pythagtriplem12  16730  pythagtriplem14  16732  pythagtriplem16  16734  remulg  21537  resubdrg  21538  prdsxmetlem  24276  xmeter  24341  bl2ioo  24700  ioo2bl  24701  ioo2blex  24702  blssioo  24703  reperf  24728  reconnlem2  24736  opnreen  24740  icopnfcnv  24860  pcoass  24944  pjthlem1  25357  ovolun  25420  shft2rab  25429  volun  25466  mbfaddlem  25581  i1fadd  25616  itg1addlem4  25620  itg2monolem1  25671  ply1divex  26062  psercnlem1  26355  reefgim  26380  tangtx  26434  efif1olem1  26471  efif1olem2  26472  efif1o  26475  relogmul  26521  argimgt0  26541  logimul  26543  ang180lem1  26739  atanlogaddlem  26843  atanlogsublem  26845  atantan  26853  ressatans  26864  emcllem6  26931  basellem9  27019  ppiub  27135  bposlem5  27219  bposlem6  27220  bposlem9  27223  chpchtlim  27410  mulog2sumlem1  27465  mulog2sumlem2  27466  selberglem2  27477  pntrmax  27495  pntpbnd1a  27516  pntpbnd2  27518  pntibndlem3  27523  pntlemb  27528  pntlemk  27537  axsegconlem7  28894  axsegconlem9  28896  axsegconlem10  28897  clwwisshclwwslemlem  29983  eucrctshift  30213  pjhthlem1  31361  staddi  32216  stadd3i  32218  cdj1i  32403  cdj3lem2b  32407  cdj3i  32411  addltmulALT  32416  dp2cl  32850  rpdp2cl  32852  raddcn  33932  subfacval3  35201  dnicld1  36485  dnibndlem2  36492  dnibndlem3  36493  dnibndlem5  36495  dnibndlem7  36497  iooelexlt  37375  cos2h  37630  tan2h  37631  poimir  37672  heicant  37674  mblfinlem2  37677  mblfinlem3  37678  ismblfin  37680  ftc1anclem3  37714  ftc1anclem4  37715  ftc1anclem6  37717  ftc1anclem7  37718  ftc1anclem8  37719  cntotbnd  37815  elre0re  42266  repncan2  42394  readdsub  42396  reltsubadd2  42399  resubsub4  42401  repnpcan  42404  reppncan  42405  pellexlem5  42845  ioomidp  45533  stoweidlem59  46076  stirlinglem10  46100  fourierdlem103  46226  fourierdlem104  46227  fouriersw  46248  sge0isum  46444  sge0seq  46463  hoidmvlelem2  46613  smflimlem4  46791  smfmullem1  46808  leaddsuble  47307  2leaddle2  47308  2elfz2melfz  47328  elfzelfzlble  47331  fmtnodvds  47554  gbegt5  47771  ltsubaddb  48525  ltsubadd2b  48527