This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulne0bbd

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	$⊢ φ \to A \in ℂ$
	mulne0bad.2	$⊢ φ \to B \in ℂ$
	mulne0bad.3	$⊢ φ \to A B \neq 0$
Assertion	mulne0bbd	$⊢ φ \to B \neq 0$

Proof

Step	Hyp	Ref	Expression
1		mulne0bad.1	$⊢ φ \to A \in ℂ$
2		mulne0bad.2	$⊢ φ \to B \in ℂ$
3		mulne0bad.3	$⊢ φ \to A B \neq 0$
4	1 2	mulne0bd	$⊢ φ \to ((A \neq 0 \land B \neq 0) \leftrightarrow A B \neq 0)$
5	3 4	mpbird	$⊢ φ \to (A \neq 0 \land B \neq 0)$
6	5	simprd	$⊢ φ \to B \neq 0$