Metamath Proof Explorer


Theorem 1lt6

Description: 1 is less than 6. (Contributed by NM, 19-Oct-2012)

Ref Expression
Assertion 1lt6
|- 1 < 6

Proof

Step Hyp Ref Expression
1 1lt2
 |-  1 < 2
2 2lt6
 |-  2 < 6
3 1re
 |-  1 e. RR
4 2re
 |-  2 e. RR
5 6re
 |-  6 e. RR
6 3 4 5 lttri
 |-  ( ( 1 < 2 /\ 2 < 6 ) -> 1 < 6 )
7 1 2 6 mp2an
 |-  1 < 6