Theorem readdcl 8295

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6075   RRcr 8168   + caddc 8172

This theorem was proved from axioms:  ax-addrcl 8266

This theorem is referenced by:  0re  8316  readdcli  8329  readdcld  8345  axltadd  8385  peano2re  8452  cnegexlem3  8493  cnegex  8494  resubcl  8580  ltleadd  8764  ltaddsublt  8889  recexap  8971  recreclt  9220  cju  9281  nnge1  9306  addltmul  9521  avglt1  9523  avglt2  9524  avgle1  9525  avgle2  9526  nzadd  9676  irradd  10025  rpaddcl  10057  xaddnemnf  10238  xaddnepnf  10239  xnegdi  10249  xaddass  10250  xltadd1  10257  iooshf  10333  ge0addcl  10362  icoshft  10371  icoshftf1o  10372  iccshftr  10375  difelfznle  10520  elfzodifsumelfzo  10597  subfzo0  10639  serfre  10899  ser3mono  10902  ser3ge0  10951  bernneq  11076  faclbnd6  11160  ccatsymb  11348  swrdswrdlem  11454  swrdccatin2  11479  readd  11612  imadd  11620  elicc4abs  11838  caubnd2  11861  maxabsle  11948  maxabslemval  11952  maxcl  11954  mulcn2  12056  climserle  12089  fsumrecl  12146  mertenslem2  12281  ege2le3  12416  eftlub  12435  efgt1  12442  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem16  13036  xmeter  15460  bl2ioo  15574  ioo2bl  15575  ioo2blex  15576  blssioo  15577  tangtx  15862  relogmul  15893  logfac  15918