Theorem negsubdi3d

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

	Ref	Expression
Hypotheses	negsubdi3d.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	negsubdi3d.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	negsubdi3d	⊢ ( 𝜑 → - ( 𝐴 − 𝐵 ) = ( - 𝐴 − - 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		negsubdi3d.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		negsubdi3d.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3	1 2	negsubdi2d	⊢ ( 𝜑 → - ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐴 ) )
4	1 2	neg2subd	⊢ ( 𝜑 → ( - 𝐴 − - 𝐵 ) = ( 𝐵 − 𝐴 ) )
5	3 4	eqtr4d	⊢ ( 𝜑 → - ( 𝐴 − 𝐵 ) = ( - 𝐴 − - 𝐵 ) )