Metamath Proof Explorer

Theorem nncan

Description: Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

Step Hyp Ref Expression
1 subsub2 
 |-  ( ( A e. CC /\ A e. CC /\ B e. CC ) -> ( A - ( A - B ) ) = ( A + ( B - A ) ) )
2 1 3anidm12 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - ( A - B ) ) = ( A + ( B - A ) ) )
3 pncan3 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + ( B - A ) ) = B )
4 2 3 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - ( A - B ) ) = B )