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  8463  cnegexlem3  8504  cnegex  8505  resubcl  8591  ltleadd  8775  ltaddsublt  8901  recexap  8983  recreclt  9232  cju  9293  nnge1  9329  addltmul  9546  avglt1  9548  avglt2  9549  avgle1  9550  avgle2  9551  nzadd  9701  irradd  10055  rpaddcl  10088  xaddnemnf  10269  xaddnepnf  10270  xnegdi  10280  xaddass  10281  xltadd1  10288  iooshf  10364  ge0addcl  10393  icoshft  10402  icoshftf1o  10403  iccshftr  10406  difelfznle  10552  elfzodifsumelfzo  10629  subfzo0  10671  serfre  10934  ser3mono  10937  ser3ge0  10986  bernneq  11111  faclbnd6  11196  ccatsymb  11384  swrdswrdlem  11490  swrdccatin2  11515  readd  11648  imadd  11656  elicc4abs  11875  caubnd2  11898  maxabsle  11985  maxabslemval  11989  maxcl  11991  mulcn2  12094  climserle  12127  fsumrecl  12184  mertenslem2  12319  ege2le3  12454  eftlub  12473  efgt1  12480  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem16  13078  xmeter  15586  bl2ioo  15700  ioo2bl  15701  ioo2blex  15702  blssioo  15703  tangtx  15989  relogmul  16021  logfac  16048  ppiqub  16194  bposlem5  16213