Metamath Proof Explorer

Theorem ltmin

Description: Two ways of saying a number is less than the minimum of two others. (Contributed by NM, 1-Sep-2006)

		Ref	Expression
	Assertion	ltmin	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A < if (B \leq C, B, C) \leftrightarrow (A < B \land A < C))$

Step	Hyp	Ref	Expression
1		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
2		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
3		rexr	$⊢ C \in ℝ \to C \in ℝ^{*}$
4		xrltmin	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A < if (B \leq C, B, C) \leftrightarrow (A < B \land A < C))$
5	1 2 3 4	syl3an	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A < if (B \leq C, B, C) \leftrightarrow (A < B \land A < C))$