Theorem negsubdi3d

Description: Distribution of negative over subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	negsubdi3d.1	$$⊢\phi \to A\in ℂ$$
	negsubdi3d.2	$$⊢\phi \to B\in ℂ$$
Assertion	negsubdi3d	$$⊢\phi \to -\left(A-B\right)=-A-\left(-B\right)$$

Proof

Step	Hyp	Ref	Expression
1		negsubdi3d.1	$$⊢\phi \to A\in ℂ$$
2		negsubdi3d.2	$$⊢\phi \to B\in ℂ$$
3	1 2	negsubdi2d	$$⊢\phi \to -\left(A-B\right)=B-A$$
4	1 2	neg2subd	$$⊢\phi \to -A-\left(-B\right)=B-A$$
5	3 4	eqtr4d	$$⊢\phi \to -\left(A-B\right)=-A-\left(-B\right)$$