Metamath Proof Explorer


Theorem pncan3d

Description: Subtraction and addition of equals. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses negidd.1 φA
pncand.2 φB
Assertion pncan3d φA+B-A=B

Proof

Step Hyp Ref Expression
1 negidd.1 φA
2 pncand.2 φB
3 pncan3 ABA+B-A=B
4 1 2 3 syl2anc φA+B-A=B