Metamath Proof Explorer


Theorem neg11d

Description: If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses negidd.1 φA
pncand.2 φB
neg11d.3 φA=B
Assertion neg11d φA=B

Proof

Step Hyp Ref Expression
1 negidd.1 φA
2 pncand.2 φB
3 neg11d.3 φA=B
4 1 2 neg11ad φA=BA=B
5 3 4 mpbid φA=B