Theorem readdcl 11121

Description: Alias for ax-addrcl 11099, for naming consistency with readdcli 11160. (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 7367  ℝcr 11037   + caddc 11041

This theorem was proved from axioms:  ax-addrcl 11099

This theorem is referenced by:  0re  11146  readdcli  11160  readdcld  11174  axltadd  11219  peano2re  11319  00id  11321  0cnALT  11381  resubcl  11458  ltaddsub  11624  leaddsub  11626  ltleadd  11633  ltaddsublt  11777  recex  11782  recp1lt1  12054  recreclt  12055  supadd  12124  cju  12155  nnge1  12205  addltmul  12413  avglt1  12415  avglt2  12416  avgle1  12417  avgle2  12418  nzadd  12575  irradd  12923  rpnnen1lem5  12931  rpaddcl  12966  xaddf  13176  xaddnemnf  13188  xaddnepnf  13189  xnegdi  13200  xaddass  13201  xadddilem  13246  iooshf  13379  ge0addcl  13413  icoshft  13426  icoshftf1o  13427  iccshftr  13439  difelfznle  13596  elfzodifsumelfzo  13686  subfzo0  13747  flbi2  13776  modcyc  13865  modadd1  13867  modsumfzodifsn  13906  serfre  13993  sermono  13996  serge0  14018  serle  14019  bernneq  14191  faclbnd6  14261  hashfun  14399  ccatsymb  14545  swrdswrdlem  14666  swrdccatin2  14691  cshweqrep  14783  cshwcsh2id  14790  readd  15088  imadd  15096  elicc4abs  15282  rddif  15303  absrdbnd  15304  caubnd2  15320  mulcn2  15558  o1add  15576  o1sub  15578  lo1add  15589  fsumrecl  15696  rerisefaccl  15982  rprisefaccl  15988  efgt1  16083  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  remulg  21587  resubdrg  21588  prdsxmetlem  24333  xmeter  24398  bl2ioo  24757  ioo2bl  24758  ioo2blex  24759  blssioo  24760  reperf  24785  reconnlem2  24793  opnreen  24797  icopnfcnv  24909  pcoass  24991  pjthlem1  25404  ovolun  25466  shft2rab  25475  volun  25512  mbfaddlem  25627  i1fadd  25662  itg1addlem4  25666  itg2monolem1  25717  ply1divex  26102  psercnlem1  26390  reefgim  26415  tangtx  26469  efif1olem1  26506  efif1olem2  26507  efif1o  26510  relogmul  26556  argimgt0  26576  logimul  26578  ang180lem1  26773  atanlogaddlem  26877  atanlogsublem  26879  atantan  26887  ressatans  26898  emcllem6  26964  basellem9  27052  ppiub  27167  bposlem5  27251  bposlem6  27252  bposlem9  27255  chpchtlim  27442  mulog2sumlem1  27497  mulog2sumlem2  27498  selberglem2  27509  pntrmax  27527  pntpbnd1a  27548  pntpbnd2  27550  pntibndlem3  27555  pntlemb  27560  pntlemk  27569  axsegconlem7  28992  axsegconlem9  28994  axsegconlem10  28995  clwwisshclwwslemlem  30083  eucrctshift  30313  pjhthlem1  31462  staddi  32317  stadd3i  32319  cdj1i  32504  cdj3lem2b  32508  cdj3i  32512  addltmulALT  32517  dp2cl  32939  rpdp2cl  32941  raddcn  34073  subfacval3  35371  dnicld1  36732  dnibndlem2  36739  dnibndlem3  36740  dnibndlem5  36742  dnibndlem7  36744  iooelexlt  37678  cos2h  37932  tan2h  37933  poimir  37974  heicant  37976  mblfinlem2  37979  mblfinlem3  37980  ismblfin  37982  ftc1anclem3  38016  ftc1anclem4  38017  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  cntotbnd  38117  elre0re  42693  repncan2  42814  readdsub  42816  reltsubadd2  42819  resubsub4  42821  repnpcan  42824  reppncan  42825  pellexlem5  43261  ioomidp  45944  stoweidlem59  46487  stirlinglem10  46511  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  sge0isum  46855  sge0seq  46874  hoidmvlelem2  47024  smflimlem4  47202  smfmullem1  47219  leaddsuble  47739  2leaddle2  47740  2elfz2melfz  47760  elfzelfzlble  47763  fmtnodvds  48001  gbegt5  48231  ltsubaddb  48984  ltsubadd2b  48986