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

Proof

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