Theorem readdcl 10614

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  (class class class)co 7150  ℝcr 10530   + caddc 10534

This theorem was proved from axioms:  ax-addrcl 10592

This theorem is referenced by:  0re  10637  readdcli  10650  readdcld  10664  axltadd  10708  peano2re  10807  00id  10809  0cnALT  10868  resubcl  10944  ltaddsub  11108  leaddsub  11110  ltleadd  11117  ltaddsublt  11261  recex  11266  recp1lt1  11532  recreclt  11533  supadd  11603  cju  11628  nnge1  11659  addltmul  11867  avglt1  11869  avglt2  11870  avgle1  11871  avgle2  11872  nzadd  12024  irradd  12366  rpnnen1lem5  12374  rpaddcl  12405  xaddf  12611  xaddnemnf  12623  xaddnepnf  12624  xnegdi  12635  xaddass  12636  xadddilem  12681  iooshf  12809  ge0addcl  12842  icoshft  12853  icoshftf1o  12854  iccshftr  12866  difelfznle  13015  elfzodifsumelfzo  13097  subfzo0  13153  flbi2  13181  modcyc  13268  modadd1  13270  modsumfzodifsn  13306  serfre  13393  sermono  13396  serge0  13418  serle  13419  bernneq  13584  faclbnd6  13653  hashfun  13792  ccatsymb  13930  swrdswrdlem  14060  swrdccatin2  14085  cshweqrep  14177  cshwcsh2id  14184  readd  14479  imadd  14487  elicc4abs  14673  rddif  14694  absrdbnd  14695  caubnd2  14711  mulcn2  14946  o1add  14964  o1sub  14966  lo1add  14977  fsumrecl  15085  rerisefaccl  15365  rprisefaccl  15371  efgt1  15463  pythagtriplem12  16157  pythagtriplem14  16159  pythagtriplem16  16161  remulg  20745  resubdrg  20746  prdsxmetlem  22972  xmeter  23037  bl2ioo  23394  ioo2bl  23395  ioo2blex  23396  blssioo  23397  reperf  23421  reconnlem2  23429  opnreen  23433  icopnfcnv  23540  pcoass  23622  pjthlem1  24034  ovolun  24094  shft2rab  24103  volun  24140  mbfaddlem  24255  i1fadd  24290  itg1addlem4  24294  itg2monolem1  24345  ply1divex  24724  psercnlem1  25007  reefgim  25032  tangtx  25085  efif1olem1  25120  efif1olem2  25121  efif1o  25124  relogmul  25169  argimgt0  25189  logimul  25191  ang180lem1  25381  atanlogaddlem  25485  atanlogsublem  25487  atantan  25495  ressatans  25506  emcllem6  25572  basellem9  25660  ppiub  25774  bposlem5  25858  bposlem6  25859  bposlem9  25862  chpchtlim  26049  mulog2sumlem1  26104  mulog2sumlem2  26105  selberglem2  26116  pntrmax  26134  pntpbnd1a  26155  pntpbnd2  26157  pntibndlem3  26162  pntlemb  26167  pntlemk  26176  axsegconlem7  26703  axsegconlem9  26705  axsegconlem10  26706  clwwisshclwwslemlem  27785  eucrctshift  28016  pjhthlem1  29162  staddi  30017  stadd3i  30019  cdj1i  30204  cdj3lem2b  30208  cdj3i  30212  addltmulALT  30217  dp2cl  30551  rpdp2cl  30553  raddcn  31167  subfacval3  32431  dnicld1  33806  dnibndlem2  33813  dnibndlem3  33814  dnibndlem5  33816  dnibndlem7  33818  iooelexlt  34637  cos2h  34877  tan2h  34878  poimir  34919  heicant  34921  mblfinlem2  34924  mblfinlem3  34925  ismblfin  34927  ftc1anclem3  34963  ftc1anclem4  34964  ftc1anclem6  34966  ftc1anclem7  34967  ftc1anclem8  34968  cntotbnd  35068  elre0re  39147  repncan2  39205  readdsub  39207  reltsubadd2  39210  resubsub4  39212  repnpcan  39215  reppncan  39216  pellexlem5  39423  ioomidp  41783  stoweidlem59  42338  stirlinglem10  42362  fourierdlem103  42488  fourierdlem104  42489  fouriersw  42510  sge0isum  42703  sge0seq  42722  hoidmvlelem2  42872  smflimlem4  43044  smfmullem1  43060  leaddsuble  43491  2leaddle2  43492  2elfz2melfz  43512  elfzelfzlble  43515  fmtnodvds  43700  gbegt5  43920  ltsubaddb  44563  ltsubadd2b  44565