Metamath Proof Explorer


Theorem 2lt6

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

Ref Expression
Assertion 2lt6 2 < 6

Proof

Step Hyp Ref Expression
1 2lt3 2 < 3
2 3lt6 3 < 6
3 2re 2 ∈ ℝ
4 3re 3 ∈ ℝ
5 6re 6 ∈ ℝ
6 3 4 5 lttri ( ( 2 < 3 ∧ 3 < 6 ) → 2 < 6 )
7 1 2 6 mp2an 2 < 6