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