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

Metamath Proof Explorer

Theorem mulne0b

Description: The product of two nonzero numbers is nonzero. (Contributed by NM, 1-Aug-2004) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion mulne0b ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ≠ 0 ∧ B ≠ 0 ↔ A ⁢ B ≠ 0

Proof

Step Hyp Ref Expression
1 neanior ⊢ A ≠ 0 ∧ B ≠ 0 ↔ ¬ A = 0 ∨ B = 0
2 mul0or ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = 0 ↔ A = 0 ∨ B = 0
3 2 necon3abid ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ≠ 0 ↔ ¬ A = 0 ∨ B = 0
4 1 3 bitr4id ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ≠ 0 ∧ B ≠ 0 ↔ A ⁢ B ≠ 0