Metamath Proof Explorer


Theorem caov32d

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 φ A S
caovd.2 φ B S
caovd.3 φ C S
caovd.com φ x S y S x F y = y F x
caovd.ass φ x S y S z S x F y F z = x F y F z
Assertion caov32d φ A F B F C = A F C F B

Proof

Step Hyp Ref Expression
1 caovd.1 φ A S
2 caovd.2 φ B S
3 caovd.3 φ C S
4 caovd.com φ x S y S x F y = y F x
5 caovd.ass φ x S y S z S x F y F z = x F y F z
6 4 2 3 caovcomd φ B F C = C F B
7 6 oveq2d φ A F B F C = A F C F B
8 5 1 2 3 caovassd φ A F B F C = A F B F C
9 5 1 3 2 caovassd φ A F C F B = A F C F B
10 7 8 9 3eqtr4d φ A F B F C = A F C F B