Theorem readdcl 10885

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7255  ℝcr 10801   + caddc 10805

This theorem was proved from axioms:  ax-addrcl 10863

This theorem is referenced by:  0re  10908  readdcli  10921  readdcld  10935  axltadd  10979  peano2re  11078  00id  11080  0cnALT  11139  resubcl  11215  ltaddsub  11379  leaddsub  11381  ltleadd  11388  ltaddsublt  11532  recex  11537  recp1lt1  11803  recreclt  11804  supadd  11873  cju  11899  nnge1  11931  addltmul  12139  avglt1  12141  avglt2  12142  avgle1  12143  avgle2  12144  nzadd  12298  irradd  12642  rpnnen1lem5  12650  rpaddcl  12681  xaddf  12887  xaddnemnf  12899  xaddnepnf  12900  xnegdi  12911  xaddass  12912  xadddilem  12957  iooshf  13087  ge0addcl  13121  icoshft  13134  icoshftf1o  13135  iccshftr  13147  difelfznle  13299  elfzodifsumelfzo  13381  subfzo0  13437  flbi2  13465  modcyc  13554  modadd1  13556  modsumfzodifsn  13592  serfre  13680  sermono  13683  serge0  13705  serle  13706  bernneq  13872  faclbnd6  13941  hashfun  14080  ccatsymb  14215  swrdswrdlem  14345  swrdccatin2  14370  cshweqrep  14462  cshwcsh2id  14469  readd  14765  imadd  14773  elicc4abs  14959  rddif  14980  absrdbnd  14981  caubnd2  14997  mulcn2  15233  o1add  15251  o1sub  15253  lo1add  15264  fsumrecl  15374  rerisefaccl  15655  rprisefaccl  15661  efgt1  15753  pythagtriplem12  16455  pythagtriplem14  16457  pythagtriplem16  16459  remulg  20724  resubdrg  20725  prdsxmetlem  23429  xmeter  23494  bl2ioo  23861  ioo2bl  23862  ioo2blex  23863  blssioo  23864  reperf  23888  reconnlem2  23896  opnreen  23900  icopnfcnv  24011  pcoass  24093  pjthlem1  24506  ovolun  24568  shft2rab  24577  volun  24614  mbfaddlem  24729  i1fadd  24764  itg1addlem4  24768  itg1addlem4OLD  24769  itg2monolem1  24820  ply1divex  25206  psercnlem1  25489  reefgim  25514  tangtx  25567  efif1olem1  25603  efif1olem2  25604  efif1o  25607  relogmul  25652  argimgt0  25672  logimul  25674  ang180lem1  25864  atanlogaddlem  25968  atanlogsublem  25970  atantan  25978  ressatans  25989  emcllem6  26055  basellem9  26143  ppiub  26257  bposlem5  26341  bposlem6  26342  bposlem9  26345  chpchtlim  26532  mulog2sumlem1  26587  mulog2sumlem2  26588  selberglem2  26599  pntrmax  26617  pntpbnd1a  26638  pntpbnd2  26640  pntibndlem3  26645  pntlemb  26650  pntlemk  26659  axsegconlem7  27194  axsegconlem9  27196  axsegconlem10  27197  clwwisshclwwslemlem  28278  eucrctshift  28508  pjhthlem1  29654  staddi  30509  stadd3i  30511  cdj1i  30696  cdj3lem2b  30700  cdj3i  30704  addltmulALT  30709  dp2cl  31056  rpdp2cl  31058  raddcn  31781  subfacval3  33051  dnicld1  34579  dnibndlem2  34586  dnibndlem3  34587  dnibndlem5  34589  dnibndlem7  34591  iooelexlt  35460  cos2h  35695  tan2h  35696  poimir  35737  heicant  35739  mblfinlem2  35742  mblfinlem3  35743  ismblfin  35745  ftc1anclem3  35779  ftc1anclem4  35780  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  cntotbnd  35881  2xp3dxp2ge1d  40090  elre0re  40212  repncan2  40286  readdsub  40288  reltsubadd2  40291  resubsub4  40293  repnpcan  40296  reppncan  40297  pellexlem5  40571  ioomidp  42942  stoweidlem59  43490  stirlinglem10  43514  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  sge0isum  43855  sge0seq  43874  hoidmvlelem2  44024  smflimlem4  44196  smfmullem1  44212  leaddsuble  44677  2leaddle2  44678  2elfz2melfz  44698  elfzelfzlble  44701  fmtnodvds  44884  gbegt5  45101  ltsubaddb  45743  ltsubadd2b  45745