Theorem readdcl 11146

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2136  (class class class)co 7385  ℝcr 11062   + caddc 11066

This theorem was proved from axioms:  ax-addrcl 11124

This theorem is referenced by:  0re  11173  readdcli  11187  readdcld  11201  axltadd  11246  peano2re  11346  00id  11348  0cnALT  11408  resubcl  11485  ltaddsub  11651  leaddsub  11653  ltleadd  11660  ltaddsublt  11804  recex  11809  recp1lt1  12080  recreclt  12081  supadd  12150  cju  12181  nnge1  12231  addltmul  12447  avglt1  12449  avglt2  12450  avgle1  12451  avgle2  12452  nzadd  12609  irradd  12964  rpnnen1lem5  12972  rpaddcl  13007  xaddf  13217  xaddnemnf  13229  xaddnepnf  13230  xnegdi  13241  xaddass  13242  xadddilem  13287  iooshf  13420  ge0addcl  13454  icoshft  13467  icoshftf1o  13468  iccshftr  13480  difelfznle  13637  elfzodifsumelfzo  13727  subfzo0  13788  flbi2  13817  modcyc  13906  modadd1  13908  modsumfzodifsn  13947  serfre  14034  sermono  14037  serge0  14059  serle  14060  bernneq  14232  faclbnd6  14302  hashfun  14440  ccatsymb  14586  swrdswrdlem  14707  swrdccatin2  14732  cshweqrep  14824  cshwcsh2id  14831  readd  15129  imadd  15137  elicc4abs  15323  rddif  15344  absrdbnd  15345  caubnd2  15361  mulcn2  15599  o1add  15617  o1sub  15619  lo1add  15630  fsumrecl  15737  rerisefaccl  16023  rprisefaccl  16029  efgt1  16124  pythagtriplem12  16838  pythagtriplem14  16840  pythagtriplem16  16842  remulg  21632  resubdrg  21633  prdsxmetlem  24401  xmeter  24466  bl2ioo  24825  ioo2bl  24826  ioo2blex  24827  blssioo  24828  reperf  24853  reconnlem2  24861  opnreen  24865  icopnfcnv  24977  pcoass  25059  pjthlem1  25472  ovolun  25534  shft2rab  25543  volun  25580  mbfaddlem  25695  i1fadd  25730  itg1addlem4  25734  itg2monolem1  25785  ply1divex  26170  psercnlem1  26458  reefgim  26483  tangtx  26540  efif1olem1  26577  efif1olem2  26578  efif1o  26581  relogmul  26627  argimgt0  26647  logimul  26649  ang180lem1  26844  atanlogaddlem  26948  atanlogsublem  26950  atantan  26958  ressatans  26969  emcllem6  27035  basellem9  27123  ppiub  27238  bposlem5  27322  bposlem6  27323  bposlem9  27326  chpchtlim  27513  mulog2sumlem1  27568  mulog2sumlem2  27569  selberglem2  27580  pntrmax  27598  pntpbnd1a  27619  pntpbnd2  27621  pntibndlem3  27626  pntlemb  27631  pntlemk  27640  axsegconlem7  29063  axsegconlem9  29065  axsegconlem10  29066  clwwisshclwwslemlem  30154  eucrctshift  30384  pjhthlem1  31533  staddi  32388  stadd3i  32390  cdj1i  32575  cdj3lem2b  32579  cdj3i  32583  addltmulALT  32588  dp2cl  33011  rpdp2cl  33013  raddcn  34180  subfacval3  35487  dnicld1  36858  dnibndlem2  36865  dnibndlem3  36866  dnibndlem5  36868  dnibndlem7  36870  iooelexlt  37804  cos2h  38058  tan2h  38059  poimir  38100  heicant  38102  mblfinlem2  38105  mblfinlem3  38106  ismblfin  38108  ftc1anclem3  38142  ftc1anclem4  38143  ftc1anclem6  38145  ftc1anclem7  38146  ftc1anclem8  38147  cntotbnd  38243  elre0re  42818  repncan2  42939  readdsub  42941  reltsubadd2  42944  resubsub4  42946  repnpcan  42949  reppncan  42950  pellexlem5  43358  ioomidp  46038  stoweidlem59  46581  stirlinglem10  46605  fourierdlem103  46731  fourierdlem104  46732  fouriersw  46753  sge0isum  46949  sge0seq  46968  hoidmvlelem2  47118  smflimlem4  47296  smfmullem1  47313  leaddsuble  47839  2leaddle2  47840  2elfz2melfz  47860  elfzelfzlble  47863  fmtnodvds  48101  gbegt5  48331  ltsubaddb  49084  ltsubadd2b  49086