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

Metamath Proof Explorer

Theorem 1lt6

Description: 1 is less than 6. (Contributed by NM, 19-Oct-2012)

		Ref	Expression
	Assertion	1lt6	$⊢ 1 < 6$

Step	Hyp	Ref	Expression
1		1lt2	$⊢ 1 < 2$
2		2lt6	$⊢ 2 < 6$
3		1re	$⊢ 1 \in ℝ$
4		2re	$⊢ 2 \in ℝ$
5		6re	$⊢ 6 \in ℝ$
6	3 4 5	lttri	$⊢ (1 < 2 \land 2 < 6) \to 1 < 6$
7	1 2 6	mp2an	$⊢ 1 < 6$