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	|- ( ph -> A e. CC )
	mulcand.2	|- ( ph -> B e. CC )
	mulcand.3	|- ( ph -> C e. CC )
	mulcand.4	|- ( ph -> C =/= 0 )
Assertion	mulcan2d	|- ( ph -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		mulcand.1	|- ( ph -> A e. CC )
2		mulcand.2	|- ( ph -> B e. CC )
3		mulcand.3	|- ( ph -> C e. CC )
4		mulcand.4	|- ( ph -> C =/= 0 )
5	1 3	mulcomd	|- ( ph -> ( A x. C ) = ( C x. A ) )
6	2 3	mulcomd	|- ( ph -> ( B x. C ) = ( C x. B ) )
7	5 6	eqeq12d	|- ( ph -> ( ( A x. C ) = ( B x. C ) <-> ( C x. A ) = ( C x. B ) ) )
8	1 2 3 4	mulcand	|- ( ph -> ( ( C x. A ) = ( C x. B ) <-> A = B ) )
9	7 8	bitrd	|- ( ph -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )