Metamath Proof Explorer

Theorem nppcan3

Description: Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
2 1 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - B ) e. CC )
3 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
4 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
5 2 3 4 addassd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) + C ) + B ) = ( ( A - B ) + ( C + B ) ) )
6 nppcan 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) + C ) + B ) = ( A + C ) )
7 5 6 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + ( C + B ) ) = ( A + C ) )