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

Theorem readdcl 6765
Description: Alias for ax-addrcl 6740, for naming consistency with readdcli 6798. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
readdcl ((A B ℝ) → (A + B) ℝ)

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 6740 1 ((A B ℝ) → (A + B) ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1390  (class class class)co 5455  cr 6670   + caddc 6674
This theorem was proved from axioms:  ax-addrcl 6740
This theorem is referenced by:  0re  6785  readdcli  6798  readdcld  6812  axltadd  6846  peano2re  6906  cnegexlem3  6945  cnegex  6946  resubcl  7031  ltleadd  7196  ltaddsublt  7315  recexap  7376  recreclt  7607  cju  7654  nnge1  7678  addltmul  7898  avglt1  7900  avglt2  7901  avgle1  7902  avgle2  7903  irradd  8315  rpaddcl  8341  iooshf  8551  ge0addcl  8580  icoshft  8588  icoshftf1o  8589  iccshftr  8592  difelfznle  8723  elfzodifsumelfzo  8787  bernneq  8982  readd  9057  imadd  9065
  Copyright terms: Public domain W3C validator