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

Theorem 1red 6932
Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1red (φ → 1 ℝ)

Proof of Theorem 1red
StepHypRef Expression
1 1re 6916 . 2 1
21a1i 9 1 (φ → 1 ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1393  cr 6778  1c1 6780
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1re 6868
This theorem is referenced by:  recgt0  7689  ltrec  7722  recp1lt1  7738  peano5nni  7790  peano2nn  7799  nn0p1gt0  8079  nn0ge2m1nn  8110  peano2z  8149  iccf1o  8734  fznatpl1  8800  elfz1b  8814  fzonn0p1p1  8931  elfzom1p1elfzo  8932  ltexp2a  9053  leexp2a  9054  leexp2r  9055  nnlesq  9102  bernneq3  9117  expnbnd  9118  expnlbnd2  9120
  Copyright terms: Public domain W3C validator