Metamath Proof Explorer

Theorem pnncan

Description: Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ
2 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
3 1 2 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B ∈ ℂ
4 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
5 subsub ⊢ A + B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ → A + B - A − C = A + B - A + C
6 3 1 4 5 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - A − C = A + B - A + C
7 pncan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A = B
8 7 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - A = B
9 8 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - A + C = B + C
10 6 9 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - A − C = B + C