# Metamath Proof Explorer

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 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-{C}={A}+{B}-{C}$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}\in ℂ$
2 subcl ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {B}-{C}\in ℂ$
3 2 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {B}-{C}\in ℂ$
4 simp3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {C}\in ℂ$
5 1 3 4 addassd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+\left({B}-{C}\right)+{C}={A}+\left({B}-{C}\right)+{C}$
6 npcan ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {B}-{C}+{C}={B}$
7 6 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {B}-{C}+{C}={B}$
8 7 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+\left({B}-{C}\right)+{C}={A}+{B}$
9 5 8 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+\left({B}-{C}\right)+{C}={A}+{B}$
10 9 oveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}+{B}-{C}\right)+{C}-{C}={A}+{B}-{C}$
11 1 3 addcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-{C}\in ℂ$
12 pncan ${⊢}\left({A}+{B}-{C}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}+{B}-{C}\right)+{C}-{C}={A}+{B}-{C}$
13 11 4 12 syl2anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}+{B}-{C}\right)+{C}-{C}={A}+{B}-{C}$
14 10 13 eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-{C}={A}+{B}-{C}$