Theorem readdcl 8148

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200  (class class class)co 6013   RRcr 8021   + caddc 8025

This theorem was proved from axioms:  ax-addrcl 8119

This theorem is referenced by:  0re  8169  readdcli  8182  readdcld  8199  axltadd  8239  peano2re  8305  cnegexlem3  8346  cnegex  8347  resubcl  8433  ltleadd  8616  ltaddsublt  8741  recexap  8823  recreclt  9070  cju  9131  nnge1  9156  addltmul  9371  avglt1  9373  avglt2  9374  avgle1  9375  avgle2  9376  nzadd  9522  irradd  9870  rpaddcl  9902  xaddnemnf  10082  xaddnepnf  10083  xnegdi  10093  xaddass  10094  xltadd1  10101  iooshf  10177  ge0addcl  10206  icoshft  10215  icoshftf1o  10216  iccshftr  10219  difelfznle  10360  elfzodifsumelfzo  10436  subfzo0  10478  serfre  10736  ser3mono  10739  ser3ge0  10788  bernneq  10912  faclbnd6  10996  ccatsymb  11169  swrdswrdlem  11275  swrdccatin2  11300  readd  11420  imadd  11428  elicc4abs  11645  caubnd2  11668  maxabsle  11755  maxabslemval  11759  maxcl  11761  mulcn2  11863  climserle  11896  fsumrecl  11952  mertenslem2  12087  ege2le3  12222  eftlub  12241  efgt1  12248  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem16  12842  xmeter  15150  bl2ioo  15264  ioo2bl  15265  ioo2blex  15266  blssioo  15267  tangtx  15552  relogmul  15583