Metamath Proof Explorer

Theorem nppcan3

Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Assertion nppcan3 ⊢ 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 addassd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + C + B = A − B + C + B
6 nppcan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + C + B = A + C
7 5 6 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + C + B = A + C