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

Metamath Proof Explorer

Theorem nncan

Description: Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

Step Hyp Ref Expression
1 subsub2 ⊢ A ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ → A − A − B = A + B - A
2 1 3anidm12 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − A − B = A + B - A
3 pncan3 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A = B
4 2 3 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − A − B = B