Metamath Proof Explorer

Theorem caov31

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 caov31 ⊢ A F B F C = C F B F A

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 1 3 2 5 caovass ⊢ A F C F B = A F C F B
7 1 3 2 4 5 caov12 ⊢ A F C F B = C F A F B
8 6 7 eqtri ⊢ A F C F B = C F A F B
9 1 2 3 4 5 caov32 ⊢ A F B F C = A F C F B
10 3 1 2 4 5 caov32 ⊢ C F A F B = C F B F A
11 3 1 2 5 caovass ⊢ C F A F B = C F A F B
12 10 11 eqtr3i ⊢ C F B F A = C F A F B
13 8 9 12 3eqtr4i ⊢ A F B F C = C F B F A