Metamath Proof Explorer

Theorem ppncan

Description: Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005)

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

Proof

Step Hyp Ref Expression
1 addcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A
2 1 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B = B + A
3 2 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - B − C = B + A - B − C
4 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
5 4 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B ∈ ℂ
6 subsub2 ⊢ A + B ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - B − C = A + B + C − B
7 5 6 syld3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - B − C = A + B + C − B
8 pnncan ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ → B + A - B − C = A + C
9 8 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + A - B − C = A + C
10 3 7 9 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B + C − B = A + C