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

Metamath Proof Explorer

Theorem subne0d

Description: Two unequal numbers have nonzero difference. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses negidd.1 ⊢ φ → A ∈ ℂ
pncand.2 ⊢ φ → B ∈ ℂ
subne0d.3 ⊢ φ → A ≠ B
Assertion subne0d ⊢ φ → A − B ≠ 0

Proof

Step Hyp Ref Expression
1 negidd.1 ⊢ φ → A ∈ ℂ
2 pncand.2 ⊢ φ → B ∈ ℂ
3 subne0d.3 ⊢ φ → A ≠ B
4 subeq0 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B = 0 ↔ A = B
5 1 2 4 syl2anc ⊢ φ → A − B = 0 ↔ A = B
6 5 necon3bid ⊢ φ → A − B ≠ 0 ↔ A ≠ B
7 3 6 mpbird ⊢ φ → A − B ≠ 0