Theorem negsubdi2i

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

	Ref	Expression
Hypotheses	negidi.1	$$⊢A\in ℂ$$
	pncan3i.2	$$⊢B\in ℂ$$
Assertion	negsubdi2i	$$⊢-\left(A-B\right)=B-A$$

Proof

Step	Hyp	Ref	Expression
1		negidi.1	$$⊢A\in ℂ$$
2		pncan3i.2	$$⊢B\in ℂ$$
3	1 2	negsubdii	$$⊢-\left(A-B\right)=-A+B$$
4	1	negcli	$$⊢-A\in ℂ$$
5	2 1	negsubi	$$⊢B+\left(-A\right)=B-A$$
6	2 4 5	addcomli	$$⊢-A+B=B-A$$
7	3 6	eqtri	$$⊢-\left(A-B\right)=B-A$$