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 e. RR
2	1	ltp1i	|- 2 < ( 2 + 1 )
3		df-3	|- 3 = ( 2 + 1 )
4	2 3	breqtrri	|- 2 < 3