Metamath Proof Explorer


Theorem 5lt7

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

Ref Expression
Assertion 5lt7 5<7

Proof

Step Hyp Ref Expression
1 5lt6 5<6
2 6lt7 6<7
3 5re 5
4 6re 6
5 7re 7
6 3 4 5 lttri 5<66<75<7
7 1 2 6 mp2an 5<7