Theorem readdcl 8253

Description: Alias for ax-addrcl 8224, for naming consistency with readdcli 8287. (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 8224	1 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2203  (class class class)co 6050   RRcr 8126   + caddc 8130

This theorem was proved from axioms:  ax-addrcl 8224

This theorem is referenced by:  0re  8274  readdcli  8287  readdcld  8303  axltadd  8343  peano2re  8409  cnegexlem3  8450  cnegex  8451  resubcl  8537  ltleadd  8720  ltaddsublt  8845  recexap  8927  recreclt  9174  cju  9235  nnge1  9260  addltmul  9475  avglt1  9477  avglt2  9478  avgle1  9479  avgle2  9480  nzadd  9630  irradd  9978  rpaddcl  10010  xaddnemnf  10190  xaddnepnf  10191  xnegdi  10201  xaddass  10202  xltadd1  10209  iooshf  10285  ge0addcl  10314  icoshft  10323  icoshftf1o  10324  iccshftr  10327  difelfznle  10469  elfzodifsumelfzo  10546  subfzo0  10588  serfre  10846  ser3mono  10849  ser3ge0  10898  bernneq  11022  faclbnd6  11106  ccatsymb  11290  swrdswrdlem  11396  swrdccatin2  11421  readd  11554  imadd  11562  elicc4abs  11779  caubnd2  11802  maxabsle  11889  maxabslemval  11893  maxcl  11895  mulcn2  11997  climserle  12030  fsumrecl  12087  mertenslem2  12222  ege2le3  12357  eftlub  12376  efgt1  12383  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem16  12977  xmeter  15301  bl2ioo  15415  ioo2bl  15416  ioo2blex  15417  blssioo  15418  tangtx  15703  relogmul  15734