This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addsubass

Description: Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ
2 subcl ⊢ B ∈ ℂ ∧ C ∈ ℂ → B − C ∈ ℂ
3 2 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B − C ∈ ℂ
4 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
5 1 3 4 addassd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B − C + C = A + B − C + C
6 npcan ⊢ B ∈ ℂ ∧ C ∈ ℂ → B - C + C = B
7 6 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B - C + C = B
8 7 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B − C + C = A + B
9 5 8 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B − C + C = A + B
10 9 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - C + C - C = A + B - C
11 1 3 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - C ∈ ℂ
12 pncan ⊢ A + B - C ∈ ℂ ∧ C ∈ ℂ → A + B - C + C - C = A + B - C
13 11 4 12 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - C + C - C = A + B - C
14 10 13 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B - C = A + B - C