Metamath Proof Explorer


Theorem 2lt7

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

Ref Expression
Assertion 2lt7 2<7

Proof

Step Hyp Ref Expression
1 2lt3 2<3
2 3lt7 3<7
3 2re 2
4 3re 3
5 7re 7
6 3 4 5 lttri 2<33<72<7
7 1 2 6 mp2an 2<7