Theorem caov411

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)$$
	caov.4	$$⊢D\in \mathrm{V}$$
Assertion	caov411	$$⊢\left(AFB\right)F\left(CFD\right)=\left(CFB\right)F\left(AFD\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	$$⊢xFy=yFx$$
5		caov.ass	$$⊢\left(xFy\right)Fz=xF\left(yFz\right)$$
6		caov.4	$$⊢D\in \mathrm{V}$$
7	1 2 3 4 5	caov31	$$⊢\left(AFB\right)FC=\left(CFB\right)FA$$
8	7	oveq1i	$$⊢\left(\left(AFB\right)FC\right)FD=\left(\left(CFB\right)FA\right)FD$$
9		ovex	$$⊢AFB\in \mathrm{V}$$
10	9 3 6 5	caovass	$$⊢\left(\left(AFB\right)FC\right)FD=\left(AFB\right)F\left(CFD\right)$$
11		ovex	$$⊢CFB\in \mathrm{V}$$
12	11 1 6 5	caovass	$$⊢\left(\left(CFB\right)FA\right)FD=\left(CFB\right)F\left(AFD\right)$$
13	8 10 12	3eqtr3i	$$⊢\left(AFB\right)F\left(CFD\right)=\left(CFB\right)F\left(AFD\right)$$