This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem negsubdi3d

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

Ref Expression
Hypotheses negsubdi3d.1 ⊢ φ → A ∈ ℂ
negsubdi3d.2 ⊢ φ → B ∈ ℂ
Assertion negsubdi3d ⊢ φ → − A − B = - A - − B

Proof

Step Hyp Ref Expression
1 negsubdi3d.1 ⊢ φ → A ∈ ℂ
2 negsubdi3d.2 ⊢ φ → B ∈ ℂ
3 1 2 negsubdi2d ⊢ φ → − A − B = B − A
4 1 2 neg2subd ⊢ φ → - A - − B = B − A
5 3 4 eqtr4d ⊢ φ → − A − B = - A - − B