Metamath Proof Explorer


Theorem 2lt9

Description: 2 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Assertion 2lt9 2 < 9

Proof

Step Hyp Ref Expression
1 2lt3 2 < 3
2 3lt9 3 < 9
3 2re 2
4 3re 3
5 9re 9
6 3 4 5 lttri 2 < 3 3 < 9 2 < 9
7 1 2 6 mp2an 2 < 9