Metamath Proof Explorer


Theorem 6lt9

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

Ref Expression
Assertion 6lt9 6 < 9

Proof

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