Theorem mulcan2d

Description: Cancellation law for multiplication. Theorem I.7 of Apostol p. 18. (Contributed by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypotheses	mulcand.1	$$⊢\phi \to A\in ℂ$$
	mulcand.2	$$⊢\phi \to B\in ℂ$$
	mulcand.3	$$⊢\phi \to C\in ℂ$$
	mulcand.4	$$⊢\phi \to C\ne 0$$
Assertion	mulcan2d	$$⊢\phi \to \left(AC=BC\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulcand.1	$$⊢\phi \to A\in ℂ$$
2		mulcand.2	$$⊢\phi \to B\in ℂ$$
3		mulcand.3	$$⊢\phi \to C\in ℂ$$
4		mulcand.4	$$⊢\phi \to C\ne 0$$
5	1 3	mulcomd	$$⊢\phi \to AC=CA$$
6	2 3	mulcomd	$$⊢\phi \to BC=CB$$
7	5 6	eqeq12d	$$⊢\phi \to \left(AC=BC\leftrightarrow CA=CB\right)$$
8	1 2 3 4	mulcand	$$⊢\phi \to \left(CA=CB\leftrightarrow A=B\right)$$
9	7 8	bitrd	$$⊢\phi \to \left(AC=BC\leftrightarrow A=B\right)$$