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