Theorem readdcl 7870

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2135  (class class class)co 5836   RRcr 7743   + caddc 7747

This theorem was proved from axioms:  ax-addrcl 7841

This theorem is referenced by:  0re  7890  readdcli  7903  readdcld  7919  axltadd  7959  peano2re  8025  cnegexlem3  8066  cnegex  8067  resubcl  8153  ltleadd  8335  ltaddsublt  8460  recexap  8541  recreclt  8786  cju  8847  nnge1  8871  addltmul  9084  avglt1  9086  avglt2  9087  avgle1  9088  avgle2  9089  nzadd  9234  irradd  9575  rpaddcl  9604  xaddnemnf  9784  xaddnepnf  9785  xnegdi  9795  xaddass  9796  xltadd1  9803  iooshf  9879  ge0addcl  9908  icoshft  9917  icoshftf1o  9918  iccshftr  9921  difelfznle  10060  elfzodifsumelfzo  10126  subfzo0  10167  serfre  10400  ser3mono  10403  ser3ge0  10442  bernneq  10564  faclbnd6  10646  readd  10797  imadd  10805  elicc4abs  11022  caubnd2  11045  maxabsle  11132  maxabslemval  11136  maxcl  11138  mulcn2  11239  climserle  11272  fsumrecl  11328  mertenslem2  11463  ege2le3  11598  eftlub  11617  efgt1  11624  pythagtriplem12  12184  pythagtriplem14  12186  pythagtriplem16  12188  xmeter  12977  bl2ioo  13083  ioo2bl  13084  ioo2blex  13085  blssioo  13086  tangtx  13300  relogmul  13331