Metamath Proof Explorer

Theorem nppcan2

Description: Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005)

Ref Expression
Assertion nppcan2 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - ( B + C ) ) + C ) = ( A - B ) )

Proof

Step Hyp Ref Expression
1 addcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B + C ) e. CC )
2 1 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B + C ) e. CC )
3 subsub 
 |-  ( ( A e. CC /\ ( B + C ) e. CC /\ C e. CC ) -> ( A - ( ( B + C ) - C ) ) = ( ( A - ( B + C ) ) + C ) )
4 2 3 syld3an2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( ( B + C ) - C ) ) = ( ( A - ( B + C ) ) + C ) )
5 pncan 
 |-  ( ( B e. CC /\ C e. CC ) -> ( ( B + C ) - C ) = B )
6 5 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B + C ) - C ) = B )
7 6 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( ( B + C ) - C ) ) = ( A - B ) )
8 4 7 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - ( B + C ) ) + C ) = ( A - B ) )