Metamath Proof Explorer

Theorem add42

Description: Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005)

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

Proof

Step Hyp Ref Expression
1 add4 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( B + D ) ) )
2 addcom 
 |-  ( ( B e. CC /\ D e. CC ) -> ( B + D ) = ( D + B ) )
3 2 ad2ant2l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( B + D ) = ( D + B ) )
4 3 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + C ) + ( B + D ) ) = ( ( A + C ) + ( D + B ) ) )
5 1 4 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( D + B ) ) )