Theorem readdcl 8033

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2175  (class class class)co 5934   RRcr 7906   + caddc 7910

This theorem was proved from axioms:  ax-addrcl 8004

This theorem is referenced by:  0re  8054  readdcli  8067  readdcld  8084  axltadd  8124  peano2re  8190  cnegexlem3  8231  cnegex  8232  resubcl  8318  ltleadd  8501  ltaddsublt  8626  recexap  8708  recreclt  8955  cju  9016  nnge1  9041  addltmul  9256  avglt1  9258  avglt2  9259  avgle1  9260  avgle2  9261  nzadd  9407  irradd  9749  rpaddcl  9781  xaddnemnf  9961  xaddnepnf  9962  xnegdi  9972  xaddass  9973  xltadd1  9980  iooshf  10056  ge0addcl  10085  icoshft  10094  icoshftf1o  10095  iccshftr  10098  difelfznle  10239  elfzodifsumelfzo  10311  subfzo0  10352  serfre  10610  ser3mono  10613  ser3ge0  10662  bernneq  10786  faclbnd6  10870  ccatsymb  11033  readd  11099  imadd  11107  elicc4abs  11324  caubnd2  11347  maxabsle  11434  maxabslemval  11438  maxcl  11440  mulcn2  11542  climserle  11575  fsumrecl  11631  mertenslem2  11766  ege2le3  11901  eftlub  11920  efgt1  11927  pythagtriplem12  12517  pythagtriplem14  12519  pythagtriplem16  12521  xmeter  14826  bl2ioo  14940  ioo2bl  14941  ioo2blex  14942  blssioo  14943  tangtx  15228  relogmul  15259