Theorem readdcl 8311

Description: Alias for ax-addrcl 8282, for naming consistency with readdcli 8345. (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 8282	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 6088   RRcr 8184   + caddc 8188

This proof depends on axioms:  ax-addrcl 8282

This theorem is used by:  0re  8332  readdcli  8345  readdcld  8361  axltadd  8401  peano2re  8469  cnegexlem3  8510  cnegex  8511  resubcl  8597  ltleadd  8781  ltaddsublt  8907  recexap  8989  recreclt  9238  cju  9299  nnge1  9336  addltmul  9553  avglt1  9555  avglt2  9556  avgle1  9557  avgle2  9558  nzadd  9708  irradd  10062  rpaddcl  10095  xaddnemnf  10276  xaddnepnf  10277  xnegdi  10287  xaddass  10288  xltadd1  10295  iooshf  10371  ge0addcl  10400  icoshft  10409  icoshftf1o  10410  iccshftr  10413  difelfznle  10559  elfzodifsumelfzo  10636  subfzo0  10678  serfre  10942  ser3mono  10945  ser3ge0  10994  bernneq  11119  faclbnd6  11204  ccatsymb  11392  swrdswrdlem  11498  swrdccatin2  11523  readd  11656  imadd  11664  elicc4abs  11883  caubnd2  11906  maxabsle  11993  maxabslemval  11997  maxcl  11999  mulcn2  12103  climserle  12136  fsumrecl  12193  mertenslem2  12328  ege2le3  12463  eftlub  12482  efgt1  12489  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem16  13087  xmeter  15662  bl2ioo  15776  ioo2bl  15777  ioo2blex  15778  blssioo  15779  tangtx  16065  relogmul  16099  logfac  16126  ppiqub  16293  bposlem5  16315  bposlem6  16316  bposlem9  16319