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 φ A
mulne0bad.2 φ B
mulne0bad.3 φ A B 0
Assertion mulne0bbd φ B 0

Proof

Step Hyp Ref Expression
1 mulne0bad.1 φ A
2 mulne0bad.2 φ B
3 mulne0bad.3 φ A B 0
4 1 2 mulne0bd φ A 0 B 0 A B 0
5 3 4 mpbird φ A 0 B 0
6 5 simprd φ B 0