Theorem readdcl 8158

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202  (class class class)co 6018   RRcr 8031   + caddc 8035

This theorem was proved from axioms:  ax-addrcl 8129

This theorem is referenced by:  0re  8179  readdcli  8192  readdcld  8209  axltadd  8249  peano2re  8315  cnegexlem3  8356  cnegex  8357  resubcl  8443  ltleadd  8626  ltaddsublt  8751  recexap  8833  recreclt  9080  cju  9141  nnge1  9166  addltmul  9381  avglt1  9383  avglt2  9384  avgle1  9385  avgle2  9386  nzadd  9532  irradd  9880  rpaddcl  9912  xaddnemnf  10092  xaddnepnf  10093  xnegdi  10103  xaddass  10104  xltadd1  10111  iooshf  10187  ge0addcl  10216  icoshft  10225  icoshftf1o  10226  iccshftr  10229  difelfznle  10370  elfzodifsumelfzo  10447  subfzo0  10489  serfre  10747  ser3mono  10750  ser3ge0  10799  bernneq  10923  faclbnd6  11007  ccatsymb  11183  swrdswrdlem  11289  swrdccatin2  11314  readd  11447  imadd  11455  elicc4abs  11672  caubnd2  11695  maxabsle  11782  maxabslemval  11786  maxcl  11788  mulcn2  11890  climserle  11923  fsumrecl  11980  mertenslem2  12115  ege2le3  12250  eftlub  12269  efgt1  12276  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem16  12870  xmeter  15179  bl2ioo  15293  ioo2bl  15294  ioo2blex  15295  blssioo  15296  tangtx  15581  relogmul  15612