Metamath Proof Explorer

Theorem npncan

Description: Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005)

Ref Expression
Assertion npncan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + B - C = A − C

Proof

Step Hyp Ref Expression
1 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
2 1 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B ∈ ℂ
3 addsubass ⊢ A − B ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + B - C = A − B + B - C
4 2 3 syld3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + B - C = A − B + B - C
5 npcan ⊢ A ∈ ℂ ∧ B ∈ ℂ → A - B + B = A
6 5 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B + B - C = A − C
7 6 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + B - C = A − C
8 4 7 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + B - C = A − C