Theorem caov31

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	caov31	$$⊢\left(AFB\right)FC=\left(CFB\right)FA$$

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	1 3 2 5	caovass	$$⊢\left(AFC\right)FB=AF\left(CFB\right)$$
7	1 3 2 4 5	caov12	$$⊢AF\left(CFB\right)=CF\left(AFB\right)$$
8	6 7	eqtri	$$⊢\left(AFC\right)FB=CF\left(AFB\right)$$
9	1 2 3 4 5	caov32	$$⊢\left(AFB\right)FC=\left(AFC\right)FB$$
10	3 1 2 4 5	caov32	$$⊢\left(CFA\right)FB=\left(CFB\right)FA$$
11	3 1 2 5	caovass	$$⊢\left(CFA\right)FB=CF\left(AFB\right)$$
12	10 11	eqtr3i	$$⊢\left(CFB\right)FA=CF\left(AFB\right)$$
13	8 9 12	3eqtr4i	$$⊢\left(AFB\right)FC=\left(CFB\right)FA$$