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	|- (ph -> 1 e. RR)

Proof of Theorem 1red

Step	Hyp	Ref	Expression
1		1re 6824	. 2 |- 1 e. RR
2	1	a1i 9	1 |- (ph -> 1 e. RR)

Syntax hints:   -> wi 4   e. wcel 1390   RRcr 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