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