Metamath Proof Explorer

Theorem pnpcan2

Description: Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006)

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

Proof

Step Hyp Ref Expression
1 addcom ⊢ A ∈ ℂ ∧ C ∈ ℂ → A + C = C + A
2 1 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C = C + A
3 addcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
4 3 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
5 2 4 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C - B + C = C + A - C + B
6 pnpcan ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ → C + A - C + B = A − B
7 6 3coml ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C + A - C + B = A − B
8 5 7 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C - B + C = A − B