Theorem negsubdi2i

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

	Ref	Expression
Hypotheses	negidi.1	|- A e. CC
	pncan3i.2	|- B e. CC
Assertion	negsubdi2i	|- -u ( A - B ) = ( B - A )

Proof

Step	Hyp	Ref	Expression
1		negidi.1	|- A e. CC
2		pncan3i.2	|- B e. CC
3	1 2	negsubdii	|- -u ( A - B ) = ( -u A + B )
4	1	negcli	|- -u A e. CC
5	2 1	negsubi	|- ( B + -u A ) = ( B - A )
6	2 4 5	addcomli	|- ( -u A + B ) = ( B - A )
7	3 6	eqtri	|- -u ( A - B ) = ( B - A )