Theorem min2

Description: The minimum of two numbers is less than or equal to the second. (Contributed by NM, 3-Aug-2007)

	Ref	Expression
Assertion	min2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( 𝐴 ≤ 𝐵 , 𝐴 , 𝐵 ) ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
2		rexr	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
3		xrmin2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → if ( 𝐴 ≤ 𝐵 , 𝐴 , 𝐵 ) ≤ 𝐵 )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( 𝐴 ≤ 𝐵 , 𝐴 , 𝐵 ) ≤ 𝐵 )