Theorem readdcl 8050

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2175  (class class class)co 5943   RRcr 7923   + caddc 7927

This theorem was proved from axioms:  ax-addrcl 8021

This theorem is referenced by:  0re  8071  readdcli  8084  readdcld  8101  axltadd  8141  peano2re  8207  cnegexlem3  8248  cnegex  8249  resubcl  8335  ltleadd  8518  ltaddsublt  8643  recexap  8725  recreclt  8972  cju  9033  nnge1  9058  addltmul  9273  avglt1  9275  avglt2  9276  avgle1  9277  avgle2  9278  nzadd  9424  irradd  9766  rpaddcl  9798  xaddnemnf  9978  xaddnepnf  9979  xnegdi  9989  xaddass  9990  xltadd1  9997  iooshf  10073  ge0addcl  10102  icoshft  10111  icoshftf1o  10112  iccshftr  10115  difelfznle  10256  elfzodifsumelfzo  10328  subfzo0  10369  serfre  10627  ser3mono  10630  ser3ge0  10679  bernneq  10803  faclbnd6  10887  ccatsymb  11056  readd  11122  imadd  11130  elicc4abs  11347  caubnd2  11370  maxabsle  11457  maxabslemval  11461  maxcl  11463  mulcn2  11565  climserle  11598  fsumrecl  11654  mertenslem2  11789  ege2le3  11924  eftlub  11943  efgt1  11950  pythagtriplem12  12540  pythagtriplem14  12542  pythagtriplem16  12544  xmeter  14850  bl2ioo  14964  ioo2bl  14965  ioo2blex  14966  blssioo  14967  tangtx  15252  relogmul  15283