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

Metamath Proof Explorer

Theorem sub4

Description: Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007)

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

Proof

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