Theorem readdcl 8306

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6085   RRcr 8179   + caddc 8183

This proof depends on axioms:  ax-addrcl 8277

This theorem is used by:  0re  8327  readdcli  8340  readdcld  8356  axltadd  8396  peano2re  8464  cnegexlem3  8505  cnegex  8506  resubcl  8592  ltleadd  8776  ltaddsublt  8902  recexap  8984  recreclt  9233  cju  9294  nnge1  9330  addltmul  9547  avglt1  9549  avglt2  9550  avgle1  9551  avgle2  9552  nzadd  9702  irradd  10056  rpaddcl  10089  xaddnemnf  10270  xaddnepnf  10271  xnegdi  10281  xaddass  10282  xltadd1  10289  iooshf  10365  ge0addcl  10394  icoshft  10403  icoshftf1o  10404  iccshftr  10407  difelfznle  10553  elfzodifsumelfzo  10630  subfzo0  10672  serfre  10936  ser3mono  10939  ser3ge0  10988  bernneq  11113  faclbnd6  11198  ccatsymb  11386  swrdswrdlem  11492  swrdccatin2  11517  readd  11650  imadd  11658  elicc4abs  11877  caubnd2  11900  maxabsle  11987  maxabslemval  11991  maxcl  11993  mulcn2  12097  climserle  12130  fsumrecl  12187  mertenslem2  12322  ege2le3  12457  eftlub  12476  efgt1  12483  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem16  13081  xmeter  15628  bl2ioo  15742  ioo2bl  15743  ioo2blex  15744  blssioo  15745  tangtx  16031  relogmul  16063  logfac  16090  ppiqub  16254  bposlem5  16276  bposlem6  16277  bposlem9  16280