Theorem readdcl 8269

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2205  (class class class)co 6058   RRcr 8142   + caddc 8146

This theorem was proved from axioms:  ax-addrcl 8240

This theorem is referenced by:  0re  8290  readdcli  8303  readdcld  8319  axltadd  8359  peano2re  8425  cnegexlem3  8466  cnegex  8467  resubcl  8553  ltleadd  8737  ltaddsublt  8862  recexap  8944  recreclt  9191  cju  9252  nnge1  9277  addltmul  9492  avglt1  9494  avglt2  9495  avgle1  9496  avgle2  9497  nzadd  9647  irradd  9996  rpaddcl  10028  xaddnemnf  10209  xaddnepnf  10210  xnegdi  10220  xaddass  10221  xltadd1  10228  iooshf  10304  ge0addcl  10333  icoshft  10342  icoshftf1o  10343  iccshftr  10346  difelfznle  10491  elfzodifsumelfzo  10568  subfzo0  10610  serfre  10870  ser3mono  10873  ser3ge0  10922  bernneq  11047  faclbnd6  11131  ccatsymb  11315  swrdswrdlem  11421  swrdccatin2  11446  readd  11579  imadd  11587  elicc4abs  11804  caubnd2  11827  maxabsle  11914  maxabslemval  11918  maxcl  11920  mulcn2  12022  climserle  12055  fsumrecl  12112  mertenslem2  12247  ege2le3  12382  eftlub  12401  efgt1  12408  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem16  13002  xmeter  15427  bl2ioo  15541  ioo2bl  15542  ioo2blex  15543  blssioo  15544  tangtx  15829  relogmul  15860