Theorem readdcl 11111

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7353  ℝcr 11027   + caddc 11031

This theorem was proved from axioms:  ax-addrcl 11089

This theorem is referenced by:  0re  11136  readdcli  11149  readdcld  11163  axltadd  11207  peano2re  11307  00id  11309  0cnALT  11369  resubcl  11446  ltaddsub  11612  leaddsub  11614  ltleadd  11621  ltaddsublt  11765  recex  11770  recp1lt1  12041  recreclt  12042  supadd  12111  cju  12142  nnge1  12174  addltmul  12378  avglt1  12380  avglt2  12381  avgle1  12382  avgle2  12383  nzadd  12541  irradd  12892  rpnnen1lem5  12900  rpaddcl  12935  xaddf  13144  xaddnemnf  13156  xaddnepnf  13157  xnegdi  13168  xaddass  13169  xadddilem  13214  iooshf  13347  ge0addcl  13381  icoshft  13394  icoshftf1o  13395  iccshftr  13407  difelfznle  13563  elfzodifsumelfzo  13652  subfzo0  13710  flbi2  13739  modcyc  13828  modadd1  13830  modsumfzodifsn  13869  serfre  13956  sermono  13959  serge0  13981  serle  13982  bernneq  14154  faclbnd6  14224  hashfun  14362  ccatsymb  14507  swrdswrdlem  14628  swrdccatin2  14653  cshweqrep  14745  cshwcsh2id  14753  readd  15051  imadd  15059  elicc4abs  15245  rddif  15266  absrdbnd  15267  caubnd2  15283  mulcn2  15521  o1add  15539  o1sub  15541  lo1add  15552  fsumrecl  15659  rerisefaccl  15942  rprisefaccl  15948  efgt1  16043  pythagtriplem12  16756  pythagtriplem14  16758  pythagtriplem16  16760  remulg  21532  resubdrg  21533  prdsxmetlem  24272  xmeter  24337  bl2ioo  24696  ioo2bl  24697  ioo2blex  24698  blssioo  24699  reperf  24724  reconnlem2  24732  opnreen  24736  icopnfcnv  24856  pcoass  24940  pjthlem1  25353  ovolun  25416  shft2rab  25425  volun  25462  mbfaddlem  25577  i1fadd  25612  itg1addlem4  25616  itg2monolem1  25667  ply1divex  26058  psercnlem1  26351  reefgim  26376  tangtx  26430  efif1olem1  26467  efif1olem2  26468  efif1o  26471  relogmul  26517  argimgt0  26537  logimul  26539  ang180lem1  26735  atanlogaddlem  26839  atanlogsublem  26841  atantan  26849  ressatans  26860  emcllem6  26927  basellem9  27015  ppiub  27131  bposlem5  27215  bposlem6  27216  bposlem9  27219  chpchtlim  27406  mulog2sumlem1  27461  mulog2sumlem2  27462  selberglem2  27473  pntrmax  27491  pntpbnd1a  27512  pntpbnd2  27514  pntibndlem3  27519  pntlemb  27524  pntlemk  27533  axsegconlem7  28886  axsegconlem9  28888  axsegconlem10  28889  clwwisshclwwslemlem  29975  eucrctshift  30205  pjhthlem1  31353  staddi  32208  stadd3i  32210  cdj1i  32395  cdj3lem2b  32399  cdj3i  32403  addltmulALT  32408  dp2cl  32833  rpdp2cl  32835  raddcn  33895  subfacval3  35161  dnicld1  36445  dnibndlem2  36452  dnibndlem3  36453  dnibndlem5  36455  dnibndlem7  36457  iooelexlt  37335  cos2h  37590  tan2h  37591  poimir  37632  heicant  37634  mblfinlem2  37637  mblfinlem3  37638  ismblfin  37640  ftc1anclem3  37674  ftc1anclem4  37675  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anclem8  37679  cntotbnd  37775  elre0re  42227  repncan2  42355  readdsub  42357  reltsubadd2  42360  resubsub4  42362  repnpcan  42365  reppncan  42366  pellexlem5  42806  ioomidp  45496  stoweidlem59  46041  stirlinglem10  46065  fourierdlem103  46191  fourierdlem104  46192  fouriersw  46213  sge0isum  46409  sge0seq  46428  hoidmvlelem2  46578  smflimlem4  46756  smfmullem1  46773  leaddsuble  47282  2leaddle2  47283  2elfz2melfz  47303  elfzelfzlble  47306  fmtnodvds  47529  gbegt5  47746  ltsubaddb  48487  ltsubadd2b  48489