Metamath Proof Explorer

Theorem subadd4

Description: Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006)

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

Proof

Step Hyp Ref Expression
1 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
2 subsub2 
 |-  ( ( ( A - B ) e. CC /\ C e. CC /\ D e. CC ) -> ( ( A - B ) - ( C - D ) ) = ( ( A - B ) + ( D - C ) ) )
3 2 3expb 
 |-  ( ( ( A - B ) e. CC /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) - ( C - D ) ) = ( ( A - B ) + ( D - C ) ) )
4 1 3 sylan 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) - ( C - D ) ) = ( ( A - B ) + ( D - C ) ) )
5 addsub4 
 |-  ( ( ( A e. CC /\ D e. CC ) /\ ( B e. CC /\ C e. CC ) ) -> ( ( A + D ) - ( B + C ) ) = ( ( A - B ) + ( D - C ) ) )
6 5 an42s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + D ) - ( B + C ) ) = ( ( A - B ) + ( D - C ) ) )
7 4 6 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) - ( C - D ) ) = ( ( A + D ) - ( B + C ) ) )