Theorem leeq2d

Description: Specialization of breq2d to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	leeq2d.1	$$⊢\phi \to A\le C$$
	leeq2d.2	$$⊢\phi \to C=D$$
	leeq2d.3	$$⊢\phi \to A\in ℝ$$
	leeq2d.4	$$⊢\phi \to C\in ℝ$$
Assertion	leeq2d	$$⊢\phi \to A\le D$$

Proof

Step	Hyp	Ref	Expression
1		leeq2d.1	$$⊢\phi \to A\le C$$
2		leeq2d.2	$$⊢\phi \to C=D$$
3		leeq2d.3	$$⊢\phi \to A\in ℝ$$
4		leeq2d.4	$$⊢\phi \to C\in ℝ$$
5	1 2	breqtrd	$$⊢\phi \to A\le D$$