Metamath Proof Explorer


Theorem add12i

Description: Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 21-Jan-1997)

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

Proof

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