Theorem int-mulsimpd

Description: MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

	Ref	Expression
Hypotheses	int-mulsimpd.1	$$⊢\phi \to B\in ℝ$$
	int-mulsimpd.2	$$⊢\phi \to A=B$$
	int-mulsimpd.3	$$⊢\phi \to B\ne 0$$
Assertion	int-mulsimpd	$$⊢\phi \to 1=\frac{A}{B}$$

Proof

Step	Hyp	Ref	Expression
1		int-mulsimpd.1	$$⊢\phi \to B\in ℝ$$
2		int-mulsimpd.2	$$⊢\phi \to A=B$$
3		int-mulsimpd.3	$$⊢\phi \to B\ne 0$$
4	1	recnd	$$⊢\phi \to B\in ℂ$$
5	4 3 2	diveq1bd	$$⊢\phi \to \frac{A}{B}=1$$
6	5	eqcomd	$$⊢\phi \to 1=\frac{A}{B}$$