Metamath Proof Explorer


Theorem negsubdii

Description: Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999)

Ref Expression
Hypotheses negidi.1 A
pncan3i.2 B
Assertion negsubdii AB=-A+B

Proof

Step Hyp Ref Expression
1 negidi.1 A
2 pncan3i.2 B
3 2 negcli B
4 1 3 negdii A+B=-A+B
5 1 2 negsubi A+B=AB
6 5 negeqi A+B=AB
7 2 negnegi B=B
8 7 oveq2i -A+B=-A+B
9 4 6 8 3eqtr3i AB=-A+B