This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subsub

Description: Law for double subtraction. (Contributed by NM, 13-May-2004)

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

Proof

Step Hyp Ref Expression
1 subsub2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( A + ( C - B ) ) )
2 addsubass 
 |-  ( ( A e. CC /\ C e. CC /\ B e. CC ) -> ( ( A + C ) - B ) = ( A + ( C - B ) ) )
3 addsub 
 |-  ( ( A e. CC /\ C e. CC /\ B e. CC ) -> ( ( A + C ) - B ) = ( ( A - B ) + C ) )
4 2 3 eqtr3d 
 |-  ( ( A e. CC /\ C e. CC /\ B e. CC ) -> ( A + ( C - B ) ) = ( ( A - B ) + C ) )
5 4 3com23 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( C - B ) ) = ( ( A - B ) + C ) )
6 1 5 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( ( A - B ) + C ) )