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

Theorem readdcl 7915
Description: Alias for ax-addrcl 7886, for naming consistency with readdcli 7948. (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 7886 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    e. wcel 2148  (class class class)co 5868   RRcr 7788    + caddc 7792
This theorem was proved from axioms:  ax-addrcl 7886
This theorem is referenced by:  0re  7935  readdcli  7948  readdcld  7964  axltadd  8004  peano2re  8070  cnegexlem3  8111  cnegex  8112  resubcl  8198  ltleadd  8380  ltaddsublt  8505  recexap  8586  recreclt  8833  cju  8894  nnge1  8918  addltmul  9131  avglt1  9133  avglt2  9134  avgle1  9135  avgle2  9136  nzadd  9281  irradd  9622  rpaddcl  9651  xaddnemnf  9831  xaddnepnf  9832  xnegdi  9842  xaddass  9843  xltadd1  9850  iooshf  9926  ge0addcl  9955  icoshft  9964  icoshftf1o  9965  iccshftr  9968  difelfznle  10108  elfzodifsumelfzo  10174  subfzo0  10215  serfre  10448  ser3mono  10451  ser3ge0  10490  bernneq  10613  faclbnd6  10695  readd  10849  imadd  10857  elicc4abs  11074  caubnd2  11097  maxabsle  11184  maxabslemval  11188  maxcl  11190  mulcn2  11291  climserle  11324  fsumrecl  11380  mertenslem2  11515  ege2le3  11650  eftlub  11669  efgt1  11676  pythagtriplem12  12245  pythagtriplem14  12247  pythagtriplem16  12249  xmeter  13569  bl2ioo  13675  ioo2bl  13676  ioo2blex  13677  blssioo  13678  tangtx  13892  relogmul  13923
  Copyright terms: Public domain W3C validator