Theorem readdcl 10609

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  (class class class)co 7135  ℝcr 10525   + caddc 10529

This theorem was proved from axioms:  ax-addrcl 10587

This theorem is referenced by:  0re  10632  readdcli  10645  readdcld  10659  axltadd  10703  peano2re  10802  00id  10804  0cnALT  10863  resubcl  10939  ltaddsub  11103  leaddsub  11105  ltleadd  11112  ltaddsublt  11256  recex  11261  recp1lt1  11527  recreclt  11528  supadd  11596  cju  11621  nnge1  11653  addltmul  11861  avglt1  11863  avglt2  11864  avgle1  11865  avgle2  11866  nzadd  12018  irradd  12360  rpnnen1lem5  12368  rpaddcl  12399  xaddf  12605  xaddnemnf  12617  xaddnepnf  12618  xnegdi  12629  xaddass  12630  xadddilem  12675  iooshf  12804  ge0addcl  12838  icoshft  12851  icoshftf1o  12852  iccshftr  12864  difelfznle  13016  elfzodifsumelfzo  13098  subfzo0  13154  flbi2  13182  modcyc  13269  modadd1  13271  modsumfzodifsn  13307  serfre  13395  sermono  13398  serge0  13420  serle  13421  bernneq  13586  faclbnd6  13655  hashfun  13794  ccatsymb  13927  swrdswrdlem  14057  swrdccatin2  14082  cshweqrep  14174  cshwcsh2id  14181  readd  14477  imadd  14485  elicc4abs  14671  rddif  14692  absrdbnd  14693  caubnd2  14709  mulcn2  14944  o1add  14962  o1sub  14964  lo1add  14975  fsumrecl  15083  rerisefaccl  15363  rprisefaccl  15369  efgt1  15461  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem16  16157  remulg  20296  resubdrg  20297  prdsxmetlem  22975  xmeter  23040  bl2ioo  23397  ioo2bl  23398  ioo2blex  23399  blssioo  23400  reperf  23424  reconnlem2  23432  opnreen  23436  icopnfcnv  23547  pcoass  23629  pjthlem1  24041  ovolun  24103  shft2rab  24112  volun  24149  mbfaddlem  24264  i1fadd  24299  itg1addlem4  24303  itg2monolem1  24354  ply1divex  24737  psercnlem1  25020  reefgim  25045  tangtx  25098  efif1olem1  25134  efif1olem2  25135  efif1o  25138  relogmul  25183  argimgt0  25203  logimul  25205  ang180lem1  25395  atanlogaddlem  25499  atanlogsublem  25501  atantan  25509  ressatans  25520  emcllem6  25586  basellem9  25674  ppiub  25788  bposlem5  25872  bposlem6  25873  bposlem9  25876  chpchtlim  26063  mulog2sumlem1  26118  mulog2sumlem2  26119  selberglem2  26130  pntrmax  26148  pntpbnd1a  26169  pntpbnd2  26171  pntibndlem3  26176  pntlemb  26181  pntlemk  26190  axsegconlem7  26717  axsegconlem9  26719  axsegconlem10  26720  clwwisshclwwslemlem  27798  eucrctshift  28028  pjhthlem1  29174  staddi  30029  stadd3i  30031  cdj1i  30216  cdj3lem2b  30220  cdj3i  30224  addltmulALT  30229  dp2cl  30582  rpdp2cl  30584  raddcn  31282  subfacval3  32549  dnicld1  33924  dnibndlem2  33931  dnibndlem3  33932  dnibndlem5  33934  dnibndlem7  33936  iooelexlt  34779  cos2h  35048  tan2h  35049  poimir  35090  heicant  35092  mblfinlem2  35095  mblfinlem3  35096  ismblfin  35098  ftc1anclem3  35132  ftc1anclem4  35133  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  cntotbnd  35234  2xp3dxp2ge1d  39387  elre0re  39462  repncan2  39520  readdsub  39522  reltsubadd2  39525  resubsub4  39527  repnpcan  39530  reppncan  39531  pellexlem5  39774  ioomidp  42151  stoweidlem59  42701  stirlinglem10  42725  fourierdlem103  42851  fourierdlem104  42852  fouriersw  42873  sge0isum  43066  sge0seq  43085  hoidmvlelem2  43235  smflimlem4  43407  smfmullem1  43423  leaddsuble  43854  2leaddle2  43855  2elfz2melfz  43875  elfzelfzlble  43878  fmtnodvds  44061  gbegt5  44279  ltsubaddb  44923  ltsubadd2b  44925