Theorem wwlemuld

Description: Natural deduction form of lemul2d . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	wwlemuld.1	$$⊢\phi \to A\in ℝ$$
	wwlemuld.2	$$⊢\phi \to B\in ℝ$$
	wwlemuld.3	$$⊢\phi \to C\in ℝ$$
	wwlemuld.4	$$⊢\phi \to CA\le CB$$
	wwlemuld.5	$$⊢\phi \to 0<C$$
Assertion	wwlemuld	$$⊢\phi \to A\le B$$

Proof

Step	Hyp	Ref	Expression
1		wwlemuld.1	$$⊢\phi \to A\in ℝ$$
2		wwlemuld.2	$$⊢\phi \to B\in ℝ$$
3		wwlemuld.3	$$⊢\phi \to C\in ℝ$$
4		wwlemuld.4	$$⊢\phi \to CA\le CB$$
5		wwlemuld.5	$$⊢\phi \to 0<C$$
6	3 5	elrpd	$$⊢\phi \to C\in {ℝ}^{+}$$
7	1 2 6	lemul2d	$$⊢\phi \to \left(A\le B\leftrightarrow CA\le CB\right)$$
8	4 7	mpbird	$$⊢\phi \to A\le B$$