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

Theorem 1red 6840
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 6824 . 2 1
21a1i 9 1 (φ → 1 ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  cr 6710  1c1 6712
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1re 6777
This theorem is referenced by:  recgt0  7597  ltrec  7630  recp1lt1  7646  peano5nni  7698  peano2nn  7707  nn0p1gt0  7987  nn0ge2m1nn  8018  peano2z  8057  iccf1o  8642  fznatpl1  8708  elfz1b  8722  fzonn0p1p1  8839  elfzom1p1elfzo  8840  ltexp2a  8960  leexp2a  8961  leexp2r  8962  nnlesq  9009  bernneq3  9024  expnbnd  9025  expnlbnd2  9027
  Copyright terms: Public domain W3C validator