ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  readdcl Unicode version

Theorem readdcl 7769
Description: Alias for ax-addrcl 7740, for naming consistency with readdcli 7802. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
readdcl  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 7740 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1481  (class class class)co 5781   RRcr 7642    + caddc 7646
This theorem was proved from axioms:  ax-addrcl 7740
This theorem is referenced by:  0re  7789  readdcli  7802  readdcld  7818  axltadd  7857  peano2re  7921  cnegexlem3  7962  cnegex  7963  resubcl  8049  ltleadd  8231  ltaddsublt  8356  recexap  8437  recreclt  8681  cju  8742  nnge1  8766  addltmul  8979  avglt1  8981  avglt2  8982  avgle1  8983  avgle2  8984  nzadd  9129  irradd  9464  rpaddcl  9493  xaddnemnf  9669  xaddnepnf  9670  xnegdi  9680  xaddass  9681  xltadd1  9688  iooshf  9764  ge0addcl  9793  icoshft  9802  icoshftf1o  9803  iccshftr  9806  difelfznle  9942  elfzodifsumelfzo  10008  subfzo0  10049  serfre  10278  ser3mono  10281  ser3ge0  10320  bernneq  10442  faclbnd6  10521  readd  10672  imadd  10680  elicc4abs  10897  caubnd2  10920  maxabsle  11007  maxabslemval  11011  maxcl  11013  mulcn2  11112  climserle  11145  fsumrecl  11201  mertenslem2  11336  ege2le3  11412  eftlub  11431  efgt1  11438  xmeter  12642  bl2ioo  12748  ioo2bl  12749  ioo2blex  12750  blssioo  12751  tangtx  12965  relogmul  12996
  Copyright terms: Public domain W3C validator