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

Metamath Proof Explorer

Theorem negsubdi2i

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

Ref Expression
Hypotheses negidi.1 ⊢ A ∈ ℂ
pncan3i.2 ⊢ B ∈ ℂ
Assertion negsubdi2i ⊢ − A − B = B − A

Proof

Step Hyp Ref Expression
1 negidi.1 ⊢ A ∈ ℂ
2 pncan3i.2 ⊢ B ∈ ℂ
3 1 2 negsubdii ⊢ − A − B = - A + B
4 1 negcli ⊢ − A ∈ ℂ
5 2 1 negsubi ⊢ B + − A = B − A
6 2 4 5 addcomli ⊢ - A + B = B − A
7 3 6 eqtri ⊢ − A − B = B − A