Theorem readdcl 8157

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202  (class class class)co 6017   RRcr 8030   + caddc 8034

This theorem was proved from axioms:  ax-addrcl 8128

This theorem is referenced by:  0re  8178  readdcli  8191  readdcld  8208  axltadd  8248  peano2re  8314  cnegexlem3  8355  cnegex  8356  resubcl  8442  ltleadd  8625  ltaddsublt  8750  recexap  8832  recreclt  9079  cju  9140  nnge1  9165  addltmul  9380  avglt1  9382  avglt2  9383  avgle1  9384  avgle2  9385  nzadd  9531  irradd  9879  rpaddcl  9911  xaddnemnf  10091  xaddnepnf  10092  xnegdi  10102  xaddass  10103  xltadd1  10110  iooshf  10186  ge0addcl  10215  icoshft  10224  icoshftf1o  10225  iccshftr  10228  difelfznle  10369  elfzodifsumelfzo  10445  subfzo0  10487  serfre  10745  ser3mono  10748  ser3ge0  10797  bernneq  10921  faclbnd6  11005  ccatsymb  11178  swrdswrdlem  11284  swrdccatin2  11309  readd  11429  imadd  11437  elicc4abs  11654  caubnd2  11677  maxabsle  11764  maxabslemval  11768  maxcl  11770  mulcn2  11872  climserle  11905  fsumrecl  11961  mertenslem2  12096  ege2le3  12231  eftlub  12250  efgt1  12257  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem16  12851  xmeter  15159  bl2ioo  15273  ioo2bl  15274  ioo2blex  15275  blssioo  15276  tangtx  15561  relogmul  15592