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

Theorem readdcl 6785
Description: Alias for ax-addrcl 6760, for naming consistency with readdcli 6818. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
readdcl  RR  RR  +  RR

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 6760 1  RR  RR  +  RR
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wcel 1390  (class class class)co 5455   RRcr 6690    + caddc 6694
This theorem was proved from axioms:  ax-addrcl 6760
This theorem is referenced by:  0re  6805  readdcli  6818  readdcld  6832  axltadd  6866  peano2re  6926  cnegexlem3  6965  cnegex  6966  resubcl  7051  ltleadd  7216  ltaddsublt  7335  recexap  7396  recreclt  7627  cju  7674  nnge1  7698  addltmul  7918  avglt1  7920  avglt2  7921  avgle1  7922  avgle2  7923  irradd  8335  rpaddcl  8361  iooshf  8571  ge0addcl  8600  icoshft  8608  icoshftf1o  8609  iccshftr  8612  difelfznle  8743  elfzodifsumelfzo  8807  bernneq  9002  readd  9077  imadd  9085
  Copyright terms: Public domain W3C validator