Theorem readdcl 8121

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200  (class class class)co 6000   RRcr 7994   + caddc 7998

This theorem was proved from axioms:  ax-addrcl 8092

This theorem is referenced by:  0re  8142  readdcli  8155  readdcld  8172  axltadd  8212  peano2re  8278  cnegexlem3  8319  cnegex  8320  resubcl  8406  ltleadd  8589  ltaddsublt  8714  recexap  8796  recreclt  9043  cju  9104  nnge1  9129  addltmul  9344  avglt1  9346  avglt2  9347  avgle1  9348  avgle2  9349  nzadd  9495  irradd  9837  rpaddcl  9869  xaddnemnf  10049  xaddnepnf  10050  xnegdi  10060  xaddass  10061  xltadd1  10068  iooshf  10144  ge0addcl  10173  icoshft  10182  icoshftf1o  10183  iccshftr  10186  difelfznle  10327  elfzodifsumelfzo  10402  subfzo0  10443  serfre  10701  ser3mono  10704  ser3ge0  10753  bernneq  10877  faclbnd6  10961  ccatsymb  11132  swrdswrdlem  11231  swrdccatin2  11256  readd  11375  imadd  11383  elicc4abs  11600  caubnd2  11623  maxabsle  11710  maxabslemval  11714  maxcl  11716  mulcn2  11818  climserle  11851  fsumrecl  11907  mertenslem2  12042  ege2le3  12177  eftlub  12196  efgt1  12203  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem16  12797  xmeter  15104  bl2ioo  15218  ioo2bl  15219  ioo2blex  15220  blssioo  15221  tangtx  15506  relogmul  15537