Theorem readdcl 11235

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151   + caddc 11155

This theorem was proved from axioms:  ax-addrcl 11213

This theorem is referenced by:  0re  11260  readdcli  11273  readdcld  11287  axltadd  11331  peano2re  11431  00id  11433  0cnALT  11493  resubcl  11570  ltaddsub  11734  leaddsub  11736  ltleadd  11743  ltaddsublt  11887  recex  11892  recp1lt1  12163  recreclt  12164  supadd  12233  cju  12259  nnge1  12291  addltmul  12499  avglt1  12501  avglt2  12502  avgle1  12503  avgle2  12504  nzadd  12662  irradd  13012  rpnnen1lem5  13020  rpaddcl  13054  xaddf  13262  xaddnemnf  13274  xaddnepnf  13275  xnegdi  13286  xaddass  13287  xadddilem  13332  iooshf  13462  ge0addcl  13496  icoshft  13509  icoshftf1o  13510  iccshftr  13522  difelfznle  13678  elfzodifsumelfzo  13766  subfzo0  13824  flbi2  13853  modcyc  13942  modadd1  13944  modsumfzodifsn  13981  serfre  14068  sermono  14071  serge0  14093  serle  14094  bernneq  14264  faclbnd6  14334  hashfun  14472  ccatsymb  14616  swrdswrdlem  14738  swrdccatin2  14763  cshweqrep  14855  cshwcsh2id  14863  readd  15161  imadd  15169  elicc4abs  15354  rddif  15375  absrdbnd  15376  caubnd2  15392  mulcn2  15628  o1add  15646  o1sub  15648  lo1add  15659  fsumrecl  15766  rerisefaccl  16049  rprisefaccl  16055  efgt1  16148  pythagtriplem12  16859  pythagtriplem14  16861  pythagtriplem16  16863  remulg  21642  resubdrg  21643  prdsxmetlem  24393  xmeter  24458  bl2ioo  24827  ioo2bl  24828  ioo2blex  24829  blssioo  24830  reperf  24854  reconnlem2  24862  opnreen  24866  icopnfcnv  24986  pcoass  25070  pjthlem1  25484  ovolun  25547  shft2rab  25556  volun  25593  mbfaddlem  25708  i1fadd  25743  itg1addlem4  25747  itg1addlem4OLD  25748  itg2monolem1  25799  ply1divex  26190  psercnlem1  26483  reefgim  26508  tangtx  26561  efif1olem1  26598  efif1olem2  26599  efif1o  26602  relogmul  26648  argimgt0  26668  logimul  26670  ang180lem1  26866  atanlogaddlem  26970  atanlogsublem  26972  atantan  26980  ressatans  26991  emcllem6  27058  basellem9  27146  ppiub  27262  bposlem5  27346  bposlem6  27347  bposlem9  27350  chpchtlim  27537  mulog2sumlem1  27592  mulog2sumlem2  27593  selberglem2  27604  pntrmax  27622  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem3  27650  pntlemb  27655  pntlemk  27664  axsegconlem7  28952  axsegconlem9  28954  axsegconlem10  28955  clwwisshclwwslemlem  30041  eucrctshift  30271  pjhthlem1  31419  staddi  32274  stadd3i  32276  cdj1i  32461  cdj3lem2b  32465  cdj3i  32469  addltmulALT  32474  dp2cl  32846  rpdp2cl  32848  raddcn  33889  subfacval3  35173  dnicld1  36454  dnibndlem2  36461  dnibndlem3  36462  dnibndlem5  36464  dnibndlem7  36466  iooelexlt  37344  cos2h  37597  tan2h  37598  poimir  37639  heicant  37641  mblfinlem2  37644  mblfinlem3  37645  ismblfin  37647  ftc1anclem3  37681  ftc1anclem4  37682  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  cntotbnd  37782  2xp3dxp2ge1d  42222  elre0re  42273  repncan2  42388  readdsub  42390  reltsubadd2  42393  resubsub4  42395  repnpcan  42398  reppncan  42399  pellexlem5  42820  ioomidp  45466  stoweidlem59  46014  stirlinglem10  46038  fourierdlem103  46164  fourierdlem104  46165  fouriersw  46186  sge0isum  46382  sge0seq  46401  hoidmvlelem2  46551  smflimlem4  46729  smfmullem1  46746  leaddsuble  47246  2leaddle2  47247  2elfz2melfz  47267  elfzelfzlble  47270  fmtnodvds  47468  gbegt5  47685  ltsubaddb  48359  ltsubadd2b  48361