Metamath Proof Explorer


Theorem nncand

Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses negidd.1 φA
pncand.2 φB
Assertion nncand φAAB=B

Proof

Step Hyp Ref Expression
1 negidd.1 φA
2 pncand.2 φB
3 nncan ABAAB=B
4 1 2 3 syl2anc φAAB=B