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 ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < if B ≤ C B C ↔ A < B ∧ A < C

Proof

Step Hyp Ref Expression
1 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
2 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
3 rexr ⊢ C ∈ ℝ → C ∈ ℝ *
4 xrltmin ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < if B ≤ C B C ↔ A < B ∧ A < C
5 1 2 3 4 syl3an ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < if B ≤ C B C ↔ A < B ∧ A < C