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 ) )