Theorem readdcl 8136

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200  (class class class)co 6007   RRcr 8009   + caddc 8013

This theorem was proved from axioms:  ax-addrcl 8107

This theorem is referenced by:  0re  8157  readdcli  8170  readdcld  8187  axltadd  8227  peano2re  8293  cnegexlem3  8334  cnegex  8335  resubcl  8421  ltleadd  8604  ltaddsublt  8729  recexap  8811  recreclt  9058  cju  9119  nnge1  9144  addltmul  9359  avglt1  9361  avglt2  9362  avgle1  9363  avgle2  9364  nzadd  9510  irradd  9853  rpaddcl  9885  xaddnemnf  10065  xaddnepnf  10066  xnegdi  10076  xaddass  10077  xltadd1  10084  iooshf  10160  ge0addcl  10189  icoshft  10198  icoshftf1o  10199  iccshftr  10202  difelfznle  10343  elfzodifsumelfzo  10419  subfzo0  10460  serfre  10718  ser3mono  10721  ser3ge0  10770  bernneq  10894  faclbnd6  10978  ccatsymb  11150  swrdswrdlem  11251  swrdccatin2  11276  readd  11395  imadd  11403  elicc4abs  11620  caubnd2  11643  maxabsle  11730  maxabslemval  11734  maxcl  11736  mulcn2  11838  climserle  11871  fsumrecl  11927  mertenslem2  12062  ege2le3  12197  eftlub  12216  efgt1  12223  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem16  12817  xmeter  15125  bl2ioo  15239  ioo2bl  15240  ioo2blex  15241  blssioo  15242  tangtx  15527  relogmul  15558