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

Metamath Proof Explorer

Theorem negsubdi2

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

Ref Expression
Assertion negsubdi2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = B − A

Proof

Step Hyp Ref Expression
1 negsubdi ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = - A + B
2 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
3 addcom ⊢ − A ∈ ℂ ∧ B ∈ ℂ → - A + B = B + − A
4 2 3 sylan ⊢ A ∈ ℂ ∧ B ∈ ℂ → - A + B = B + − A
5 negsub ⊢ B ∈ ℂ ∧ A ∈ ℂ → B + − A = B − A
6 5 ancoms ⊢ A ∈ ℂ ∧ B ∈ ℂ → B + − A = B − A
7 1 4 6 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = B − A