Metamath Proof Explorer


Theorem add4i

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

Ref Expression
Hypotheses add.1
|- A e. CC
add.2
|- B e. CC
add.3
|- C e. CC
add4.4
|- D e. CC
Assertion add4i
|- ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( B + D ) )

Proof

Step Hyp Ref Expression
1 add.1
 |-  A e. CC
2 add.2
 |-  B e. CC
3 add.3
 |-  C e. CC
4 add4.4
 |-  D e. CC
5 add4
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( B + D ) ) )
6 1 2 3 4 5 mp4an
 |-  ( ( A + B ) + ( C + D ) ) = ( ( A + C ) + ( B + D ) )