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

Metamath Proof Explorer

Theorem divne0d

Description: The ratio of nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses div1d.1 ⊢ φ → A ∈ ℂ
divcld.2 ⊢ φ → B ∈ ℂ
divne0d.3 ⊢ φ → A ≠ 0
divne0d.4 ⊢ φ → B ≠ 0
Assertion divne0d ⊢ φ → A B ≠ 0

Proof

Step Hyp Ref Expression
1 div1d.1 ⊢ φ → A ∈ ℂ
2 divcld.2 ⊢ φ → B ∈ ℂ
3 divne0d.3 ⊢ φ → A ≠ 0
4 divne0d.4 ⊢ φ → B ≠ 0
5 divne0 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ≠ 0
6 1 3 2 4 5 syl22anc ⊢ φ → A B ≠ 0