Theorem mulne0bad

Description: A factor of a nonzero complex number is nonzero. Partial converse of mulne0d and consequence of mulne0bd . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	mulne0bad.1	|- ( ph -> A e. CC )
	mulne0bad.2	|- ( ph -> B e. CC )
	mulne0bad.3	|- ( ph -> ( A x. B ) =/= 0 )
Assertion	mulne0bad	|- ( ph -> A =/= 0 )

Proof

Step	Hyp	Ref	Expression
1		mulne0bad.1	|- ( ph -> A e. CC )
2		mulne0bad.2	|- ( ph -> B e. CC )
3		mulne0bad.3	|- ( ph -> ( A x. B ) =/= 0 )
4	1 2	mulne0bd	|- ( ph -> ( ( A =/= 0 /\ B =/= 0 ) <-> ( A x. B ) =/= 0 ) )
5	3 4	mpbird	|- ( ph -> ( A =/= 0 /\ B =/= 0 ) )
6	5	simpld	|- ( ph -> A =/= 0 )