Metamath Proof Explorer


Theorem caov32

Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995)

Ref Expression
Hypotheses caov.1 A V
caov.2 B V
caov.3 C V
caov.com x F y = y F x
caov.ass x F y F z = x F y F z
Assertion caov32 A F B F C = A F C F B

Proof

Step Hyp Ref Expression
1 caov.1 A V
2 caov.2 B V
3 caov.3 C V
4 caov.com x F y = y F x
5 caov.ass x F y F z = x F y F z
6 2 3 4 caovcom B F C = C F B
7 6 oveq2i A F B F C = A F C F B
8 1 2 3 5 caovass A F B F C = A F B F C
9 1 3 2 5 caovass A F C F B = A F C F B
10 7 8 9 3eqtr4i A F B F C = A F C F B