Theorem readdcl 7879

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2136  (class class class)co 5842   RRcr 7752   + caddc 7756

This theorem was proved from axioms:  ax-addrcl 7850

This theorem is referenced by:  0re  7899  readdcli  7912  readdcld  7928  axltadd  7968  peano2re  8034  cnegexlem3  8075  cnegex  8076  resubcl  8162  ltleadd  8344  ltaddsublt  8469  recexap  8550  recreclt  8795  cju  8856  nnge1  8880  addltmul  9093  avglt1  9095  avglt2  9096  avgle1  9097  avgle2  9098  nzadd  9243  irradd  9584  rpaddcl  9613  xaddnemnf  9793  xaddnepnf  9794  xnegdi  9804  xaddass  9805  xltadd1  9812  iooshf  9888  ge0addcl  9917  icoshft  9926  icoshftf1o  9927  iccshftr  9930  difelfznle  10070  elfzodifsumelfzo  10136  subfzo0  10177  serfre  10410  ser3mono  10413  ser3ge0  10452  bernneq  10575  faclbnd6  10657  readd  10811  imadd  10819  elicc4abs  11036  caubnd2  11059  maxabsle  11146  maxabslemval  11150  maxcl  11152  mulcn2  11253  climserle  11286  fsumrecl  11342  mertenslem2  11477  ege2le3  11612  eftlub  11631  efgt1  11638  pythagtriplem12  12207  pythagtriplem14  12209  pythagtriplem16  12211  xmeter  13076  bl2ioo  13182  ioo2bl  13183  ioo2blex  13184  blssioo  13185  tangtx  13399  relogmul  13430