Theorem readdcl 7937

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148  (class class class)co 5875   RRcr 7810   + caddc 7814

This theorem was proved from axioms:  ax-addrcl 7908

This theorem is referenced by:  0re  7957  readdcli  7970  readdcld  7987  axltadd  8027  peano2re  8093  cnegexlem3  8134  cnegex  8135  resubcl  8221  ltleadd  8403  ltaddsublt  8528  recexap  8610  recreclt  8857  cju  8918  nnge1  8942  addltmul  9155  avglt1  9157  avglt2  9158  avgle1  9159  avgle2  9160  nzadd  9305  irradd  9646  rpaddcl  9677  xaddnemnf  9857  xaddnepnf  9858  xnegdi  9868  xaddass  9869  xltadd1  9876  iooshf  9952  ge0addcl  9981  icoshft  9990  icoshftf1o  9991  iccshftr  9994  difelfznle  10135  elfzodifsumelfzo  10201  subfzo0  10242  serfre  10475  ser3mono  10478  ser3ge0  10517  bernneq  10641  faclbnd6  10724  readd  10878  imadd  10886  elicc4abs  11103  caubnd2  11126  maxabsle  11213  maxabslemval  11217  maxcl  11219  mulcn2  11320  climserle  11353  fsumrecl  11409  mertenslem2  11544  ege2le3  11679  eftlub  11698  efgt1  11705  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  xmeter  13939  bl2ioo  14045  ioo2bl  14046  ioo2blex  14047  blssioo  14048  tangtx  14262  relogmul  14293