Theorem 2lt3

Description: 2 is less than 3. (Contributed by NM, 26-Sep-2010)

	Ref	Expression
Assertion	2lt3	$$⊢2<3$$

Proof

Step	Hyp	Ref	Expression
1		2re	$$⊢2\in ℝ$$
2	1	ltp1i	$$⊢2<2+1$$
3		df-3	$$⊢3=2+1$$
4	2 3	breqtrri	$$⊢2<3$$