Theorem readdcl 7529

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1439  (class class class)co 5666   RRcr 7410   + caddc 7414

This theorem was proved from axioms:  ax-addrcl 7503

This theorem is referenced by:  0re  7549  readdcli  7562  readdcld  7578  axltadd  7617  peano2re  7679  cnegexlem3  7720  cnegex  7721  resubcl  7807  ltleadd  7985  ltaddsublt  8109  recexap  8183  recreclt  8422  cju  8482  nnge1  8506  addltmul  8713  avglt1  8715  avglt2  8716  avgle1  8717  avgle2  8718  nzadd  8863  irradd  9192  rpaddcl  9218  iooshf  9431  ge0addcl  9460  icoshft  9468  icoshftf1o  9469  iccshftr  9472  difelfznle  9607  elfzodifsumelfzo  9673  subfzo0  9714  serfre  9962  isermono  9967  ser3ge0  10013  bernneq  10135  faclbnd6  10213  readd  10364  imadd  10372  elicc4abs  10588  caubnd2  10611  maxabsle  10698  maxabslemval  10702  maxcl  10704  mulcn2  10762  climserle  10795  fsumrecl  10856  mertenslem2  10991  ege2le3  11022  eftlub  11041  efgt1  11048