Theorem min1d

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

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

Proof

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