Metamath Proof Explorer

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	$⊢ φ \to A \in S$
		caovd.2	$⊢ φ \to B \in S$
		caovd.3	$⊢ φ \to C \in S$
		caovd.com	$⊢ (φ \land (x \in S \land y \in S)) \to x F y = y F x$
		caovd.ass	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x F y) F z = x F (y F z)$
	Assertion	caov31d	$⊢ φ \to (A F B) F C = (C F B) F A$

Proof

Step	Hyp	Ref	Expression
1		caovd.1	$⊢ φ \to A \in S$
2		caovd.2	$⊢ φ \to B \in S$
3		caovd.3	$⊢ φ \to C \in S$
4		caovd.com	$⊢ (φ \land (x \in S \land y \in S)) \to x F y = y F x$
5		caovd.ass	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x F y) F z = x F (y F z)$
6	4 1 3	caovcomd	$⊢ φ \to A F C = C F A$
7	6	oveq1d	$⊢ φ \to (A F C) F B = (C F A) F B$
8	1 2 3 4 5	caov32d	$⊢ φ \to (A F B) F C = (A F C) F B$
9	3 2 1 4 5	caov32d	$⊢ φ \to (C F B) F A = (C F A) F B$
10	7 8 9	3eqtr4d	$⊢ φ \to (A F B) F C = (C F B) F A$