Theorem readdcl 8305

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

Assertion

Ref	Expression
readdcl	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )

Proof of Theorem readdcl

Step	Hyp	Ref	Expression
1		ax-addrcl 8276	1 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6085   RRcr 8178   + caddc 8182

This proof depends on axioms:  ax-addrcl 8276

This theorem is used by:  0re  8326  readdcli  8339  readdcld  8355  axltadd  8395  peano2re  8462  cnegexlem3  8503  cnegex  8504  resubcl  8590  ltleadd  8774  ltaddsublt  8899  recexap  8981  recreclt  9230  cju  9291  nnge1  9327  addltmul  9542  avglt1  9544  avglt2  9545  avgle1  9546  avgle2  9547  nzadd  9697  irradd  10046  rpaddcl  10078  xaddnemnf  10259  xaddnepnf  10260  xnegdi  10270  xaddass  10271  xltadd1  10278  iooshf  10354  ge0addcl  10383  icoshft  10392  icoshftf1o  10393  iccshftr  10396  difelfznle  10542  elfzodifsumelfzo  10619  subfzo0  10661  serfre  10921  ser3mono  10924  ser3ge0  10973  bernneq  11098  faclbnd6  11182  ccatsymb  11370  swrdswrdlem  11476  swrdccatin2  11501  readd  11634  imadd  11642  elicc4abs  11860  caubnd2  11883  maxabsle  11970  maxabslemval  11974  maxcl  11976  mulcn2  12078  climserle  12111  fsumrecl  12168  mertenslem2  12303  ege2le3  12438  eftlub  12457  efgt1  12464  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem16  13058  xmeter  15537  bl2ioo  15651  ioo2bl  15652  ioo2blex  15653  blssioo  15654  tangtx  15939  relogmul  15970  logfac  15995