Theorem readdcl 7739

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480  (class class class)co 5767   RRcr 7612   + caddc 7616

This theorem was proved from axioms:  ax-addrcl 7710

This theorem is referenced by:  0re  7759  readdcli  7772  readdcld  7788  axltadd  7827  peano2re  7891  cnegexlem3  7932  cnegex  7933  resubcl  8019  ltleadd  8201  ltaddsublt  8326  recexap  8407  recreclt  8651  cju  8712  nnge1  8736  addltmul  8949  avglt1  8951  avglt2  8952  avgle1  8953  avgle2  8954  nzadd  9099  irradd  9431  rpaddcl  9458  xaddnemnf  9633  xaddnepnf  9634  xnegdi  9644  xaddass  9645  xltadd1  9652  iooshf  9728  ge0addcl  9757  icoshft  9766  icoshftf1o  9767  iccshftr  9770  difelfznle  9905  elfzodifsumelfzo  9971  subfzo0  10012  serfre  10241  ser3mono  10244  ser3ge0  10283  bernneq  10405  faclbnd6  10483  readd  10634  imadd  10642  elicc4abs  10859  caubnd2  10882  maxabsle  10969  maxabslemval  10973  maxcl  10975  mulcn2  11074  climserle  11107  fsumrecl  11163  mertenslem2  11298  ege2le3  11366  eftlub  11385  efgt1  11392  xmeter  12594  bl2ioo  12700  ioo2bl  12701  ioo2blex  12702  blssioo  12703  tangtx  12908