Theorem 7lt8

Description: 7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013)

	Ref	Expression
Assertion	7lt8	⊢ 7 < 8

Proof

Step	Hyp	Ref	Expression
1		7re	⊢ 7 ∈ ℝ
2	1	ltp1i	⊢ 7 < ( 7 + 1 )
3		df-8	⊢ 8 = ( 7 + 1 )
4	2 3	breqtrri	⊢ 7 < 8