This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caov4d

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)$
		caovd.4	$⊢ φ \to D \in S$
		caovd.cl	$⊢ (φ \land (x \in S \land y \in S)) \to x F y \in S$
	Assertion	caov4d	$⊢ φ \to (A F B) F (C F D) = (A F C) F (B F D)$

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		caovd.4	$⊢ φ \to D \in S$
7		caovd.cl	$⊢ (φ \land (x \in S \land y \in S)) \to x F y \in S$
8	2 3 6 4 5	caov12d	$⊢ φ \to B F (C F D) = C F (B F D)$
9	8	oveq2d	$⊢ φ \to A F (B F (C F D)) = A F (C F (B F D))$
10	7 3 6	caovcld	$⊢ φ \to C F D \in S$
11	5 1 2 10	caovassd	$⊢ φ \to (A F B) F (C F D) = A F (B F (C F D))$
12	7 2 6	caovcld	$⊢ φ \to B F D \in S$
13	5 1 3 12	caovassd	$⊢ φ \to (A F C) F (B F D) = A F (C F (B F D))$
14	9 11 13	3eqtr4d	$⊢ φ \to (A F B) F (C F D) = (A F C) F (B F D)$