# 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}\in \mathrm{V}$
caov.2 ${⊢}{B}\in \mathrm{V}$
caov.3 ${⊢}{C}\in \mathrm{V}$
caov.com ${⊢}{x}{F}{y}={y}{F}{x}$
caov.ass ${⊢}\left({x}{F}{y}\right){F}{z}={x}{F}\left({y}{F}{z}\right)$
Assertion caov12 ${⊢}{A}{F}\left({B}{F}{C}\right)={B}{F}\left({A}{F}{C}\right)$

### Proof

Step Hyp Ref Expression
1 caov.1 ${⊢}{A}\in \mathrm{V}$
2 caov.2 ${⊢}{B}\in \mathrm{V}$
3 caov.3 ${⊢}{C}\in \mathrm{V}$
4 caov.com ${⊢}{x}{F}{y}={y}{F}{x}$
5 caov.ass ${⊢}\left({x}{F}{y}\right){F}{z}={x}{F}\left({y}{F}{z}\right)$
6 1 2 4 caovcom ${⊢}{A}{F}{B}={B}{F}{A}$
7 6 oveq1i ${⊢}\left({A}{F}{B}\right){F}{C}=\left({B}{F}{A}\right){F}{C}$
8 1 2 3 5 caovass ${⊢}\left({A}{F}{B}\right){F}{C}={A}{F}\left({B}{F}{C}\right)$
9 2 1 3 5 caovass ${⊢}\left({B}{F}{A}\right){F}{C}={B}{F}\left({A}{F}{C}\right)$
10 7 8 9 3eqtr3i ${⊢}{A}{F}\left({B}{F}{C}\right)={B}{F}\left({A}{F}{C}\right)$