Metamath Proof Explorer


Theorem 3lt4

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

Ref Expression
Assertion 3lt4 3 < 4

Proof

Step Hyp Ref Expression
1 3re 3 ∈ ℝ
2 1 ltp1i 3 < ( 3 + 1 )
3 df-4 4 = ( 3 + 1 )
4 2 3 breqtrri 3 < 4