Metamath Proof Explorer

Theorem sub32

Description: Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005)

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

Proof

Step Hyp Ref Expression
1 addcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B + C ) = ( C + B ) )
2 1 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B + C ) = ( C + B ) )
3 2 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B + C ) ) = ( A - ( C + B ) ) )
4 subsub4 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) - C ) = ( A - ( B + C ) ) )
5 subsub4 
 |-  ( ( A e. CC /\ C e. CC /\ B e. CC ) -> ( ( A - C ) - B ) = ( A - ( C + B ) ) )
6 5 3com23 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) - B ) = ( A - ( C + B ) ) )
7 3 4 6 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) - C ) = ( ( A - C ) - B ) )