Metamath Proof Explorer

Theorem nppcan

Description: Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005)

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

Proof

Step Hyp Ref Expression
1 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
2 1 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B ∈ ℂ
3 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
4 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
5 2 3 4 add32d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + C + B = A − B + B + C
6 npcan ⊢ A ∈ ℂ ∧ B ∈ ℂ → A - B + B = A
7 6 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B + B + C = A + C
8 7 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + B + C = A + C
9 5 8 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + C + B = A + C