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 ∈ ℝ
2	1	ltp1i	⊢ 2 < ( 2 + 1 )
3		df-3	⊢ 3 = ( 2 + 1 )
4	2 3	breqtrri	⊢ 2 < 3