Theorem readdcl 11121

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7368  ℝcr 11037   + caddc 11041

This theorem was proved from axioms:  ax-addrcl 11099

This theorem is referenced by:  0re  11146  readdcli  11159  readdcld  11173  axltadd  11218  peano2re  11318  00id  11320  0cnALT  11380  resubcl  11457  ltaddsub  11623  leaddsub  11625  ltleadd  11632  ltaddsublt  11776  recex  11781  recp1lt1  12052  recreclt  12053  supadd  12122  cju  12153  nnge1  12185  addltmul  12389  avglt1  12391  avglt2  12392  avgle1  12393  avgle2  12394  nzadd  12551  irradd  12898  rpnnen1lem5  12906  rpaddcl  12941  xaddf  13151  xaddnemnf  13163  xaddnepnf  13164  xnegdi  13175  xaddass  13176  xadddilem  13221  iooshf  13354  ge0addcl  13388  icoshft  13401  icoshftf1o  13402  iccshftr  13414  difelfznle  13570  elfzodifsumelfzo  13659  subfzo0  13720  flbi2  13749  modcyc  13838  modadd1  13840  modsumfzodifsn  13879  serfre  13966  sermono  13969  serge0  13991  serle  13992  bernneq  14164  faclbnd6  14234  hashfun  14372  ccatsymb  14518  swrdswrdlem  14639  swrdccatin2  14664  cshweqrep  14756  cshwcsh2id  14763  readd  15061  imadd  15069  elicc4abs  15255  rddif  15276  absrdbnd  15277  caubnd2  15293  mulcn2  15531  o1add  15549  o1sub  15551  lo1add  15562  fsumrecl  15669  rerisefaccl  15952  rprisefaccl  15958  efgt1  16053  pythagtriplem12  16766  pythagtriplem14  16768  pythagtriplem16  16770  remulg  21574  resubdrg  21575  prdsxmetlem  24324  xmeter  24389  bl2ioo  24748  ioo2bl  24749  ioo2blex  24750  blssioo  24751  reperf  24776  reconnlem2  24784  opnreen  24788  icopnfcnv  24908  pcoass  24992  pjthlem1  25405  ovolun  25468  shft2rab  25477  volun  25514  mbfaddlem  25629  i1fadd  25664  itg1addlem4  25668  itg2monolem1  25719  ply1divex  26110  psercnlem1  26403  reefgim  26428  tangtx  26482  efif1olem1  26519  efif1olem2  26520  efif1o  26523  relogmul  26569  argimgt0  26589  logimul  26591  ang180lem1  26787  atanlogaddlem  26891  atanlogsublem  26893  atantan  26901  ressatans  26912  emcllem6  26979  basellem9  27067  ppiub  27183  bposlem5  27267  bposlem6  27268  bposlem9  27271  chpchtlim  27458  mulog2sumlem1  27513  mulog2sumlem2  27514  selberglem2  27525  pntrmax  27543  pntpbnd1a  27564  pntpbnd2  27566  pntibndlem3  27571  pntlemb  27576  pntlemk  27585  axsegconlem7  29008  axsegconlem9  29010  axsegconlem10  29011  clwwisshclwwslemlem  30100  eucrctshift  30330  pjhthlem1  31478  staddi  32333  stadd3i  32335  cdj1i  32520  cdj3lem2b  32524  cdj3i  32528  addltmulALT  32533  dp2cl  32971  rpdp2cl  32973  raddcn  34106  subfacval3  35402  dnicld1  36691  dnibndlem2  36698  dnibndlem3  36699  dnibndlem5  36701  dnibndlem7  36703  iooelexlt  37606  cos2h  37851  tan2h  37852  poimir  37893  heicant  37895  mblfinlem2  37898  mblfinlem3  37899  ismblfin  37901  ftc1anclem3  37935  ftc1anclem4  37936  ftc1anclem6  37938  ftc1anclem7  37939  ftc1anclem8  37940  cntotbnd  38036  elre0re  42613  repncan2  42741  readdsub  42743  reltsubadd2  42746  resubsub4  42748  repnpcan  42751  reppncan  42752  pellexlem5  43179  ioomidp  45863  stoweidlem59  46406  stirlinglem10  46430  fourierdlem103  46556  fourierdlem104  46557  fouriersw  46578  sge0isum  46774  sge0seq  46793  hoidmvlelem2  46943  smflimlem4  47121  smfmullem1  47138  leaddsuble  47646  2leaddle2  47647  2elfz2melfz  47667  elfzelfzlble  47670  fmtnodvds  47893  gbegt5  48110  ltsubaddb  48863  ltsubadd2b  48865