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 φAB
Assertion subne0d φAB0

Proof

Step Hyp Ref Expression
1 negidd.1 φA
2 pncand.2 φB
3 subne0d.3 φAB
4 subeq0 ABAB=0A=B
5 1 2 4 syl2anc φAB=0A=B
6 5 necon3bid φAB0AB
7 3 6 mpbird φAB0