Theorem readdcl 8311

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6088   RRcr 8184   + caddc 8188

This proof depends on axioms:  ax-addrcl 8282

This theorem is used by:  0re  8332  readdcli  8345  readdcld  8361  axltadd  8401  peano2re  8469  cnegexlem3  8510  cnegex  8511  resubcl  8597  ltleadd  8781  ltaddsublt  8907  recexap  8989  recreclt  9238  cju  9299  nnge1  9336  addltmul  9553  avglt1  9555  avglt2  9556  avgle1  9557  avgle2  9558  nzadd  9706  irradd  10061  rpaddcl  10094  xaddnemnf  10275  xaddnepnf  10276  xnegdi  10286  xaddass  10287  xltadd1  10294  iooshf  10370  ge0addcl  10399  icoshft  10408  icoshftf1o  10409  iccshftr  10412  difelfznle  10558  elfzodifsumelfzo  10635  subfzo0  10677  serfre  10941  ser3mono  10944  ser3ge0  10993  bernneq  11118  faclbnd6  11203  ccatsymb  11391  swrdswrdlem  11497  swrdccatin2  11522  readd  11655  imadd  11663  elicc4abs  11882  caubnd2  11905  maxabsle  11992  maxabslemval  11996  maxcl  11998  mulcn2  12102  climserle  12135  fsumrecl  12192  mertenslem2  12327  ege2le3  12462  eftlub  12481  efgt1  12488  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem16  13086  xmeter  15679  bl2ioo  15793  ioo2bl  15794  ioo2blex  15795  blssioo  15796  tangtx  16082  relogmul  16116  logfac  16143  ppiqub  16310  bposlem5  16332  bposlem6  16333  bposlem9  16336