Theorem mulcan2ad

Description: Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcan2d . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	mulcanad.1	$$⊢\phi \to A\in ℂ$$
	mulcanad.2	$$⊢\phi \to B\in ℂ$$
	mulcanad.3	$$⊢\phi \to C\in ℂ$$
	mulcanad.4	$$⊢\phi \to C\ne 0$$
	mulcan2ad.5	$$⊢\phi \to AC=BC$$
Assertion	mulcan2ad	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		mulcanad.1	$$⊢\phi \to A\in ℂ$$
2		mulcanad.2	$$⊢\phi \to B\in ℂ$$
3		mulcanad.3	$$⊢\phi \to C\in ℂ$$
4		mulcanad.4	$$⊢\phi \to C\ne 0$$
5		mulcan2ad.5	$$⊢\phi \to AC=BC$$
6	1 2 3 4	mulcan2d	$$⊢\phi \to \left(AC=BC\leftrightarrow A=B\right)$$
7	5 6	mpbid	$$⊢\phi \to A=B$$