Metamath Proof Explorer

Theorem caov12

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

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 2 4 caovcom ⊢ A F B = B F A
7 6 oveq1i ⊢ A F B F C = B F A F C
8 1 2 3 5 caovass ⊢ A F B F C = A F B F C
9 2 1 3 5 caovass ⊢ B F A F C = B F A F C
10 7 8 9 3eqtr3i ⊢ A F B F C = B F A F C