Metamath Proof Explorer


Theorem 4lt8

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

Ref Expression
Assertion 4lt8 4 < 8

Proof

Step Hyp Ref Expression
1 4lt5 4 < 5
2 5lt8 5 < 8
3 4re 4
4 5re 5
5 8re 8
6 3 4 5 lttri 4 < 5 5 < 8 4 < 8
7 1 2 6 mp2an 4 < 8