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\in ℝ$$
2	1	ltp1i	$$⊢7<7+1$$
3		df-8	$$⊢8=7+1$$
4	2 3	breqtrri	$$⊢7<8$$