Metamath Proof Explorer

Theorem npncan3

Description: Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ
2 subcl ⊢ C ∈ ℂ ∧ A ∈ ℂ → C − A ∈ ℂ
3 2 ancoms ⊢ A ∈ ℂ ∧ C ∈ ℂ → C − A ∈ ℂ
4 3 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C − A ∈ ℂ
5 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
6 addsub ⊢ A ∈ ℂ ∧ C − A ∈ ℂ ∧ B ∈ ℂ → A + C − A - B = A − B + C - A
7 1 4 5 6 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C − A - B = A − B + C - A
8 pncan3 ⊢ A ∈ ℂ ∧ C ∈ ℂ → A + C - A = C
9 8 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C - A = C
10 9 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C − A - B = C − B
11 7 10 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + C - A = C − B