Metamath Proof Explorer

Theorem ppncan

Description: Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005)

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

Proof

Step Hyp Ref Expression
1 addcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
2 1 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + B ) = ( B + A ) )
3 2 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - ( B - C ) ) = ( ( B + A ) - ( B - C ) ) )
4 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
5 4 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + B ) e. CC )
6 subsub2 
 |-  ( ( ( A + B ) e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - ( B - C ) ) = ( ( A + B ) + ( C - B ) ) )
7 5 6 syld3an1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - ( B - C ) ) = ( ( A + B ) + ( C - B ) ) )
8 pnncan 
 |-  ( ( B e. CC /\ A e. CC /\ C e. CC ) -> ( ( B + A ) - ( B - C ) ) = ( A + C ) )
9 8 3com12 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B + A ) - ( B - C ) ) = ( A + C ) )
10 3 7 9 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + ( C - B ) ) = ( A + C ) )