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 e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - C ) = ( A + ( B - C ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
2 subcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
3 2 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
4 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
5 1 3 4 addassd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + ( B - C ) ) + C ) = ( A + ( ( B - C ) + C ) ) )
6 npcan 
 |-  ( ( B e. CC /\ C e. CC ) -> ( ( B - C ) + C ) = B )
7 6 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B - C ) + C ) = B )
8 7 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( ( B - C ) + C ) ) = ( A + B ) )
9 5 8 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + ( B - C ) ) + C ) = ( A + B ) )
10 9 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A + ( B - C ) ) + C ) - C ) = ( ( A + B ) - C ) )
11 1 3 addcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( B - C ) ) e. CC )
12 pncan 
 |-  ( ( ( A + ( B - C ) ) e. CC /\ C e. CC ) -> ( ( ( A + ( B - C ) ) + C ) - C ) = ( A + ( B - C ) ) )
13 11 4 12 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A + ( B - C ) ) + C ) - C ) = ( A + ( B - C ) ) )
14 10 13 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - C ) = ( A + ( B - C ) ) )