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