Theorem readdcl 8201

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202  (class class class)co 6028   RRcr 8074   + caddc 8078

This theorem was proved from axioms:  ax-addrcl 8172

This theorem is referenced by:  0re  8222  readdcli  8235  readdcld  8251  axltadd  8291  peano2re  8357  cnegexlem3  8398  cnegex  8399  resubcl  8485  ltleadd  8668  ltaddsublt  8793  recexap  8875  recreclt  9122  cju  9183  nnge1  9208  addltmul  9423  avglt1  9425  avglt2  9426  avgle1  9427  avgle2  9428  nzadd  9576  irradd  9924  rpaddcl  9956  xaddnemnf  10136  xaddnepnf  10137  xnegdi  10147  xaddass  10148  xltadd1  10155  iooshf  10231  ge0addcl  10260  icoshft  10269  icoshftf1o  10270  iccshftr  10273  difelfznle  10415  elfzodifsumelfzo  10492  subfzo0  10534  serfre  10792  ser3mono  10795  ser3ge0  10844  bernneq  10968  faclbnd6  11052  ccatsymb  11228  swrdswrdlem  11334  swrdccatin2  11359  readd  11492  imadd  11500  elicc4abs  11717  caubnd2  11740  maxabsle  11827  maxabslemval  11831  maxcl  11833  mulcn2  11935  climserle  11968  fsumrecl  12025  mertenslem2  12160  ege2le3  12295  eftlub  12314  efgt1  12321  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem16  12915  xmeter  15230  bl2ioo  15344  ioo2bl  15345  ioo2blex  15346  blssioo  15347  tangtx  15632  relogmul  15663