Metamath Proof Explorer


Theorem 4lt6

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

Ref Expression
Assertion 4lt6 4<6

Proof

Step Hyp Ref Expression
1 4lt5 4<5
2 5lt6 5<6
3 4re 4
4 5re 5
5 6re 6
6 3 4 5 lttri 4<55<64<6
7 1 2 6 mp2an 4<6