Metamath Proof Explorer

Theorem pnpcan

Description: Cancellation law for mixed addition and subtraction. (Contributed by NM, 4-Mar-2005) (Revised by Mario Carneiro, 27-May-2016) (Proof shortened by SN, 13-Nov-2023)

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

Proof

Step Hyp Ref Expression
1 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
2 subsub4 
 |-  ( ( ( A + B ) e. CC /\ A e. CC /\ C e. CC ) -> ( ( ( A + B ) - A ) - C ) = ( ( A + B ) - ( A + C ) ) )
3 1 2 stoic4a 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A + B ) - A ) - C ) = ( ( A + B ) - ( A + C ) ) )
4 pncan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - A ) = B )
5 4 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - A ) = B )
6 5 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A + B ) - A ) - C ) = ( B - C ) )
7 3 6 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - ( A + C ) ) = ( B - C ) )