Theorem readdcl 11182

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2141  (class class class)co 7410  ℝcr 11098   + caddc 11102

This theorem was proved from axioms:  ax-addrcl 11160

This theorem is referenced by:  0re  11209  readdcli  11223  readdcld  11237  axltadd  11282  peano2re  11382  00id  11384  0cnALT  11444  resubcl  11521  ltaddsub  11687  leaddsub  11689  ltleadd  11696  ltaddsublt  11840  recex  11845  recp1lt1  12112  recreclt  12113  supadd  12182  cju  12213  nnge1  12263  addltmul  12479  avglt1  12481  avglt2  12482  avgle1  12483  avgle2  12484  nzadd  12641  irradd  12996  rpnnen1lem5  13004  rpaddcl  13039  xaddf  13249  xaddnemnf  13261  xaddnepnf  13262  xnegdi  13273  xaddass  13274  xadddilem  13319  iooshf  13452  ge0addcl  13486  icoshft  13499  icoshftf1o  13500  iccshftr  13512  difelfznle  13670  elfzodifsumelfzo  13760  subfzo0  13821  flbi2  13850  modcyc  13939  modadd1  13941  modsumfzodifsn  13980  serfre  14067  sermono  14070  serge0  14092  serle  14093  bernneq  14265  faclbnd6  14335  hashfun  14474  ccatsymb  14620  swrdswrdlem  14741  swrdccatin2  14766  cshweqrep  14858  cshwcsh2id  14865  readd  15177  imadd  15185  elicc4abs  15371  rddif  15392  absrdbnd  15393  caubnd2  15409  mulcn2  15647  o1add  15665  o1sub  15667  lo1add  15678  fsumrecl  15785  rerisefaccl  16071  rprisefaccl  16077  efgt1  16171  pythagtriplem12  16885  pythagtriplem14  16887  pythagtriplem16  16889  remulg  21736  resubdrg  21737  prdsxmetlem  24504  xmeter  24569  bl2ioo  24928  ioo2bl  24929  ioo2blex  24930  blssioo  24931  reperf  24956  reconnlem2  24964  opnreen  24968  icopnfcnv  25080  pcoass  25162  pjthlem1  25575  ovolun  25637  shft2rab  25646  volun  25683  mbfaddlem  25798  i1fadd  25833  itg1addlem4  25837  itg2monolem1  25888  ply1divex  26273  psercnlem1  26564  reefgim  26589  tangtx  26646  efif1olem1  26683  efif1olem2  26684  efif1o  26687  relogmul  26733  argimgt0  26753  logimul  26755  ang180lem1  26950  atanlogaddlem  27054  atanlogsublem  27056  atantan  27064  ressatans  27075  emcllem6  27141  basellem9  27229  ppiub  27344  bposlem5  27428  bposlem6  27429  bposlem9  27432  chpchtlim  27619  mulog2sumlem1  27674  mulog2sumlem2  27675  selberglem2  27686  pntrmax  27704  pntpbnd1a  27725  pntpbnd2  27727  pntibndlem3  27732  pntlemb  27737  pntlemk  27746  axsegconlem7  29239  axsegconlem9  29241  axsegconlem10  29242  clwwisshclwwslemlem  30330  eucrctshift  30560  pjhthlem1  31709  staddi  32564  stadd3i  32566  cdj1i  32751  cdj3lem2b  32755  cdj3i  32759  addltmulALT  32764  dp2cl  33165  rpdp2cl  33167  raddcn  34285  subfacval3  35647  dnicld1  37027  dnibndlem2  37034  dnibndlem3  37035  dnibndlem5  37037  dnibndlem7  37039  iooelexlt  37974  cos2h  38228  tan2h  38229  poimir  38270  heicant  38272  mblfinlem2  38275  mblfinlem3  38276  ismblfin  38278  ftc1anclem3  38312  ftc1anclem4  38313  ftc1anclem6  38315  ftc1anclem7  38316  ftc1anclem8  38317  cntotbnd  38413  elre0re  42990  repncan2  43111  readdsub  43113  reltsubadd2  43116  resubsub4  43118  repnpcan  43121  reppncan  43122  pellexlem5  43530  ioomidp  46200  stoweidlem59  46743  stirlinglem10  46767  fourierdlem103  46893  fourierdlem104  46894  fouriersw  46915  sge0isum  47111  sge0seq  47130  hoidmvlelem2  47280  smflimlem4  47458  smfmullem1  47475  leaddsuble  48001  2leaddle2  48002  2elfz2melfz  48022  elfzelfzlble  48025  fmtnodvds  48263  gbegt5  48493  ltsubaddb  49261  ltsubadd2b  49263