Theorem caov32

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	$$⊢xFy=yFx$$
	caov.ass	$$⊢\left(xFy\right)Fz=xF\left(yFz\right)$$
Assertion	caov32	$$⊢\left(AFB\right)FC=\left(AFC\right)FB$$

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	$$⊢xFy=yFx$$
5		caov.ass	$$⊢\left(xFy\right)Fz=xF\left(yFz\right)$$
6	2 3 4	caovcom	$$⊢BFC=CFB$$
7	6	oveq2i	$$⊢AF\left(BFC\right)=AF\left(CFB\right)$$
8	1 2 3 5	caovass	$$⊢\left(AFB\right)FC=AF\left(BFC\right)$$
9	1 3 2 5	caovass	$$⊢\left(AFC\right)FB=AF\left(CFB\right)$$
10	7 8 9	3eqtr4i	$$⊢\left(AFB\right)FC=\left(AFC\right)FB$$