Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 30-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | caovd.1 | ||
caovd.2 | |||
caovd.3 | |||
caovd.com | |||
caovd.ass | |||
Assertion | caov32d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caovd.1 | ||
2 | caovd.2 | ||
3 | caovd.3 | ||
4 | caovd.com | ||
5 | caovd.ass | ||
6 | 4 2 3 | caovcomd | |
7 | 6 | oveq2d | |
8 | 5 1 2 3 | caovassd | |
9 | 5 1 3 2 | caovassd | |
10 | 7 8 9 | 3eqtr4d |