Theorem readdcl 7746

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480  (class class class)co 5774   RRcr 7619   + caddc 7623

This theorem was proved from axioms:  ax-addrcl 7717

This theorem is referenced by:  0re  7766  readdcli  7779  readdcld  7795  axltadd  7834  peano2re  7898  cnegexlem3  7939  cnegex  7940  resubcl  8026  ltleadd  8208  ltaddsublt  8333  recexap  8414  recreclt  8658  cju  8719  nnge1  8743  addltmul  8956  avglt1  8958  avglt2  8959  avgle1  8960  avgle2  8961  nzadd  9106  irradd  9438  rpaddcl  9465  xaddnemnf  9640  xaddnepnf  9641  xnegdi  9651  xaddass  9652  xltadd1  9659  iooshf  9735  ge0addcl  9764  icoshft  9773  icoshftf1o  9774  iccshftr  9777  difelfznle  9912  elfzodifsumelfzo  9978  subfzo0  10019  serfre  10248  ser3mono  10251  ser3ge0  10290  bernneq  10412  faclbnd6  10490  readd  10641  imadd  10649  elicc4abs  10866  caubnd2  10889  maxabsle  10976  maxabslemval  10980  maxcl  10982  mulcn2  11081  climserle  11114  fsumrecl  11170  mertenslem2  11305  ege2le3  11377  eftlub  11396  efgt1  11403  xmeter  12605  bl2ioo  12711  ioo2bl  12712  ioo2blex  12713  blssioo  12714  tangtx  12919