Theorem caov31d

Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Hypotheses	caovd.1	$$⊢\phi \to A\in S$$
	caovd.2	$$⊢\phi \to B\in S$$
	caovd.3	$$⊢\phi \to C\in S$$
	caovd.com	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xFy=yFx$$
	caovd.ass	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\wedge z\in S\right)\right)\to \left(xFy\right)Fz=xF\left(yFz\right)$$
Assertion	caov31d	$$⊢\phi \to \left(AFB\right)FC=\left(CFB\right)FA$$

Proof

Step	Hyp	Ref	Expression
1		caovd.1	$$⊢\phi \to A\in S$$
2		caovd.2	$$⊢\phi \to B\in S$$
3		caovd.3	$$⊢\phi \to C\in S$$
4		caovd.com	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xFy=yFx$$
5		caovd.ass	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\wedge z\in S\right)\right)\to \left(xFy\right)Fz=xF\left(yFz\right)$$
6	4 1 3	caovcomd	$$⊢\phi \to AFC=CFA$$
7	6	oveq1d	$$⊢\phi \to \left(AFC\right)FB=\left(CFA\right)FB$$
8	1 2 3 4 5	caov32d	$$⊢\phi \to \left(AFB\right)FC=\left(AFC\right)FB$$
9	3 2 1 4 5	caov32d	$$⊢\phi \to \left(CFB\right)FA=\left(CFA\right)FB$$
10	7 8 9	3eqtr4d	$$⊢\phi \to \left(AFB\right)FC=\left(CFB\right)FA$$