Theorem mulcanad

Description: Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcand . (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$$
	mulcanad.5	$$⊢\phi \to CA=CB$$
Assertion	mulcanad	$$⊢\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		mulcanad.5	$$⊢\phi \to CA=CB$$
6	1 2 3 4	mulcand	$$⊢\phi \to \left(CA=CB\leftrightarrow A=B\right)$$
7	5 6	mpbid	$$⊢\phi \to A=B$$