Theorem min2d

Description: The minimum of two numbers is less than or equal to the second. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	min2d.1	$$⊢\phi \to A\in ℝ$$
	min2d.2	$$⊢\phi \to B\in ℝ$$
Assertion	min2d	$$⊢\phi \to if\left(A\le B,A,B\right)\le B$$

Proof

Step	Hyp	Ref	Expression
1		min2d.1	$$⊢\phi \to A\in ℝ$$
2		min2d.2	$$⊢\phi \to B\in ℝ$$
3		min2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to if\left(A\le B,A,B\right)\le B$$
4	1 2 3	syl2anc	$$⊢\phi \to if\left(A\le B,A,B\right)\le B$$