Metamath Proof Explorer

Theorem lemin

Description: Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by NM, 3-Aug-2007)

Ref Expression
Assertion lemin ⊢ 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 xrlemin ⊢ 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