Theorem readdcl 11190

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  (class class class)co 7406  ℝcr 11106   + caddc 11110

This theorem was proved from axioms:  ax-addrcl 11168

This theorem is referenced by:  0re  11213  readdcli  11226  readdcld  11240  axltadd  11284  peano2re  11384  00id  11386  0cnALT  11445  resubcl  11521  ltaddsub  11685  leaddsub  11687  ltleadd  11694  ltaddsublt  11838  recex  11843  recp1lt1  12109  recreclt  12110  supadd  12179  cju  12205  nnge1  12237  addltmul  12445  avglt1  12447  avglt2  12448  avgle1  12449  avgle2  12450  nzadd  12607  irradd  12954  rpnnen1lem5  12962  rpaddcl  12993  xaddf  13200  xaddnemnf  13212  xaddnepnf  13213  xnegdi  13224  xaddass  13225  xadddilem  13270  iooshf  13400  ge0addcl  13434  icoshft  13447  icoshftf1o  13448  iccshftr  13460  difelfznle  13612  elfzodifsumelfzo  13695  subfzo0  13751  flbi2  13779  modcyc  13868  modadd1  13870  modsumfzodifsn  13906  serfre  13994  sermono  13997  serge0  14019  serle  14020  bernneq  14189  faclbnd6  14256  hashfun  14394  ccatsymb  14529  swrdswrdlem  14651  swrdccatin2  14676  cshweqrep  14768  cshwcsh2id  14776  readd  15070  imadd  15078  elicc4abs  15263  rddif  15284  absrdbnd  15285  caubnd2  15301  mulcn2  15537  o1add  15555  o1sub  15557  lo1add  15568  fsumrecl  15677  rerisefaccl  15958  rprisefaccl  15964  efgt1  16056  pythagtriplem12  16756  pythagtriplem14  16758  pythagtriplem16  16760  remulg  21152  resubdrg  21153  prdsxmetlem  23866  xmeter  23931  bl2ioo  24300  ioo2bl  24301  ioo2blex  24302  blssioo  24303  reperf  24327  reconnlem2  24335  opnreen  24339  icopnfcnv  24450  pcoass  24532  pjthlem1  24946  ovolun  25008  shft2rab  25017  volun  25054  mbfaddlem  25169  i1fadd  25204  itg1addlem4  25208  itg1addlem4OLD  25209  itg2monolem1  25260  ply1divex  25646  psercnlem1  25929  reefgim  25954  tangtx  26007  efif1olem1  26043  efif1olem2  26044  efif1o  26047  relogmul  26092  argimgt0  26112  logimul  26114  ang180lem1  26304  atanlogaddlem  26408  atanlogsublem  26410  atantan  26418  ressatans  26429  emcllem6  26495  basellem9  26583  ppiub  26697  bposlem5  26781  bposlem6  26782  bposlem9  26785  chpchtlim  26972  mulog2sumlem1  27027  mulog2sumlem2  27028  selberglem2  27039  pntrmax  27057  pntpbnd1a  27078  pntpbnd2  27080  pntibndlem3  27085  pntlemb  27090  pntlemk  27099  axsegconlem7  28171  axsegconlem9  28173  axsegconlem10  28174  clwwisshclwwslemlem  29256  eucrctshift  29486  pjhthlem1  30632  staddi  31487  stadd3i  31489  cdj1i  31674  cdj3lem2b  31678  cdj3i  31682  addltmulALT  31687  dp2cl  32034  rpdp2cl  32036  raddcn  32898  subfacval3  34169  dnicld1  35337  dnibndlem2  35344  dnibndlem3  35345  dnibndlem5  35347  dnibndlem7  35349  iooelexlt  36232  cos2h  36468  tan2h  36469  poimir  36510  heicant  36512  mblfinlem2  36515  mblfinlem3  36516  ismblfin  36518  ftc1anclem3  36552  ftc1anclem4  36553  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  cntotbnd  36653  2xp3dxp2ge1d  41011  elre0re  41173  repncan2  41252  readdsub  41254  reltsubadd2  41257  resubsub4  41259  repnpcan  41262  reppncan  41263  pellexlem5  41557  ioomidp  44214  stoweidlem59  44762  stirlinglem10  44786  fourierdlem103  44912  fourierdlem104  44913  fouriersw  44934  sge0isum  45130  sge0seq  45149  hoidmvlelem2  45299  smflimlem4  45477  smfmullem1  45494  leaddsuble  45992  2leaddle2  45993  2elfz2melfz  46013  elfzelfzlble  46016  fmtnodvds  46199  gbegt5  46416  ltsubaddb  47149  ltsubadd2b  47151