Metamath Proof Explorer

Theorem npncan

Description: Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005)

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

Proof

Step Hyp Ref Expression
1 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
2 1 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - B ) e. CC )
3 addsubass 
 |-  ( ( ( A - B ) e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) + B ) - C ) = ( ( A - B ) + ( B - C ) ) )
4 2 3 syld3an1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) + B ) - C ) = ( ( A - B ) + ( B - C ) ) )
5 npcan 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + B ) = A )
6 5 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A - B ) + B ) - C ) = ( A - C ) )
7 6 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) + B ) - C ) = ( A - C ) )
8 4 7 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + ( B - C ) ) = ( A - C ) )