This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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