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 ) ) |
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 ) ) |