Metamath Proof Explorer


Theorem 7lt8

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

Ref Expression
Assertion 7lt8 7 < 8

Proof

Step Hyp Ref Expression
1 7re 7
2 1 ltp1i 7 < 7 + 1
3 df-8 8 = 7 + 1
4 2 3 breqtrri 7 < 8