caov4

Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995)

Step	Hyp	Ref	Expression
1		caov.1	$⊢ A \in V$
2		caov.2	$⊢ B \in V$
3		caov.3	$⊢ C \in V$
4		caov.com	$⊢ x F y = y F x$
5		caov.ass	$⊢ (x F y) F z = x F (y F z)$
6		caov.4	$⊢ D \in V$
7	2 3 6 4 5	caov12	$⊢ B F (C F D) = C F (B F D)$
8	7	oveq2i	$⊢ A F (B F (C F D)) = A F (C F (B F D))$
9		ovex	$⊢ C F D \in V$
10	1 2 9 5	caovass	$⊢ (A F B) F (C F D) = A F (B F (C F D))$
11		ovex	$⊢ B F D \in V$
12	1 3 11 5	caovass	$⊢ (A F C) F (B F D) = A F (C F (B F D))$
13	8 10 12	3eqtr4i	$⊢ (A F B) F (C F D) = (A F C) F (B F D)$

Metamath Proof Explorer