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	|- ( ph -> A e. S )
	caovd.2	|- ( ph -> B e. S )
	caovd.3	|- ( ph -> C e. S )
	caovd.com	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )
	caovd.ass	|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )
	caovd.4	|- ( ph -> D e. S )
	caovd.cl	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )
Assertion	caov4d	|- ( ph -> ( ( A F B ) F ( C F D ) ) = ( ( A F C ) F ( B F D ) ) )

Proof

Step	Hyp	Ref	Expression
1		caovd.1	|- ( ph -> A e. S )
2		caovd.2	|- ( ph -> B e. S )
3		caovd.3	|- ( ph -> C e. S )
4		caovd.com	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )
5		caovd.ass	|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )
6		caovd.4	|- ( ph -> D e. S )
7		caovd.cl	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )
8	2 3 6 4 5	caov12d	|- ( ph -> ( B F ( C F D ) ) = ( C F ( B F D ) ) )
9	8	oveq2d	|- ( ph -> ( A F ( B F ( C F D ) ) ) = ( A F ( C F ( B F D ) ) ) )
10	7 3 6	caovcld	|- ( ph -> ( C F D ) e. S )
11	5 1 2 10	caovassd	|- ( ph -> ( ( A F B ) F ( C F D ) ) = ( A F ( B F ( C F D ) ) ) )
12	7 2 6	caovcld	|- ( ph -> ( B F D ) e. S )
13	5 1 3 12	caovassd	|- ( ph -> ( ( A F C ) F ( B F D ) ) = ( A F ( C F ( B F D ) ) ) )
14	9 11 13	3eqtr4d	|- ( ph -> ( ( A F B ) F ( C F D ) ) = ( ( A F C ) F ( B F D ) ) )