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

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

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 6780 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 6710   + caddc 6714
This theorem was proved from axioms:  ax-addrcl 6780
This theorem is referenced by:  0re  6825  readdcli  6838  readdcld  6852  axltadd  6886  peano2re  6946  cnegexlem3  6985  cnegex  6986  resubcl  7071  ltleadd  7236  ltaddsublt  7355  recexap  7416  recreclt  7647  cju  7694  nnge1  7718  addltmul  7938  avglt1  7940  avglt2  7941  avgle1  7942  avgle2  7943  irradd  8355  rpaddcl  8381  iooshf  8591  ge0addcl  8620  icoshft  8628  icoshftf1o  8629  iccshftr  8632  difelfznle  8763  elfzodifsumelfzo  8827  bernneq  9022  readd  9097  imadd  9105
  Copyright terms: Public domain W3C validator