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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
2		rexr	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
3		rexr	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ* )
4		xrlemin	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶 ) ) )
5	1 2 3 4	syl3an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶 ) ) )