Theorem readdcl 11171

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  (class class class)co 7400  ℝcr 11087   + caddc 11091

This theorem was proved from axioms:  ax-addrcl 11149

This theorem is referenced by:  0re  11198  readdcli  11212  readdcld  11226  axltadd  11271  peano2re  11371  00id  11373  0cnALT  11433  resubcl  11510  ltaddsub  11676  leaddsub  11678  ltleadd  11685  ltaddsublt  11829  recex  11834  recp1lt1  12104  recreclt  12105  supadd  12174  cju  12205  nnge1  12255  addltmul  12471  avglt1  12473  avglt2  12474  avgle1  12475  avgle2  12476  nzadd  12633  irradd  12988  rpnnen1lem5  12996  rpaddcl  13031  xaddf  13241  xaddnemnf  13253  xaddnepnf  13254  xnegdi  13265  xaddass  13266  xadddilem  13311  iooshf  13444  ge0addcl  13478  icoshft  13491  icoshftf1o  13492  iccshftr  13504  difelfznle  13661  elfzodifsumelfzo  13751  subfzo0  13812  flbi2  13841  modcyc  13930  modadd1  13932  modsumfzodifsn  13971  serfre  14058  sermono  14061  serge0  14083  serle  14084  bernneq  14256  faclbnd6  14326  hashfun  14464  ccatsymb  14610  swrdswrdlem  14731  swrdccatin2  14756  cshweqrep  14848  cshwcsh2id  14855  readd  15167  imadd  15175  elicc4abs  15361  rddif  15382  absrdbnd  15383  caubnd2  15399  mulcn2  15637  o1add  15655  o1sub  15657  lo1add  15668  fsumrecl  15775  rerisefaccl  16061  rprisefaccl  16067  efgt1  16162  pythagtriplem12  16876  pythagtriplem14  16878  pythagtriplem16  16880  remulg  21717  resubdrg  21718  prdsxmetlem  24486  xmeter  24551  bl2ioo  24910  ioo2bl  24911  ioo2blex  24912  blssioo  24913  reperf  24938  reconnlem2  24946  opnreen  24950  icopnfcnv  25062  pcoass  25144  pjthlem1  25557  ovolun  25619  shft2rab  25628  volun  25665  mbfaddlem  25780  i1fadd  25815  itg1addlem4  25819  itg2monolem1  25870  ply1divex  26255  psercnlem1  26546  reefgim  26571  tangtx  26628  efif1olem1  26665  efif1olem2  26666  efif1o  26669  relogmul  26715  argimgt0  26735  logimul  26737  ang180lem1  26932  atanlogaddlem  27036  atanlogsublem  27038  atantan  27046  ressatans  27057  emcllem6  27123  basellem9  27211  ppiub  27326  bposlem5  27410  bposlem6  27411  bposlem9  27414  chpchtlim  27601  mulog2sumlem1  27656  mulog2sumlem2  27657  selberglem2  27668  pntrmax  27686  pntpbnd1a  27707  pntpbnd2  27709  pntibndlem3  27714  pntlemb  27719  pntlemk  27728  axsegconlem7  29182  axsegconlem9  29184  axsegconlem10  29185  clwwisshclwwslemlem  30273  eucrctshift  30503  pjhthlem1  31652  staddi  32507  stadd3i  32509  cdj1i  32694  cdj3lem2b  32698  cdj3i  32702  addltmulALT  32707  dp2cl  33112  rpdp2cl  33114  raddcn  34236  subfacval3  35552  dnicld1  36923  dnibndlem2  36930  dnibndlem3  36931  dnibndlem5  36933  dnibndlem7  36935  iooelexlt  37868  cos2h  38122  tan2h  38123  poimir  38164  heicant  38166  mblfinlem2  38169  mblfinlem3  38170  ismblfin  38172  ftc1anclem3  38206  ftc1anclem4  38207  ftc1anclem6  38209  ftc1anclem7  38210  ftc1anclem8  38211  cntotbnd  38307  elre0re  42882  repncan2  43003  readdsub  43005  reltsubadd2  43008  resubsub4  43010  repnpcan  43013  reppncan  43014  pellexlem5  43422  ioomidp  46088  stoweidlem59  46631  stirlinglem10  46655  fourierdlem103  46781  fourierdlem104  46782  fouriersw  46803  sge0isum  46999  sge0seq  47018  hoidmvlelem2  47168  smflimlem4  47346  smfmullem1  47363  leaddsuble  47889  2leaddle2  47890  2elfz2melfz  47910  elfzelfzlble  47913  fmtnodvds  48151  gbegt5  48381  ltsubaddb  49145  ltsubadd2b  49147