Theorem caovass

Description: Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 26-May-2014)

	Ref	Expression
Hypotheses	caovass.1	|- A e. _V
	caovass.2	|- B e. _V
	caovass.3	|- C e. _V
	caovass.4	|- ( ( x F y ) F z ) = ( x F ( y F z ) )
Assertion	caovass	|- ( ( A F B ) F C ) = ( A F ( B F C ) )

Proof

Step	Hyp	Ref	Expression
1		caovass.1	|- A e. _V
2		caovass.2	|- B e. _V
3		caovass.3	|- C e. _V
4		caovass.4	|- ( ( x F y ) F z ) = ( x F ( y F z ) )
5		tru	|- T.
6	4	a1i	|- ( ( T. /\ ( x e. _V /\ y e. _V /\ z e. _V ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )
7	6	caovassg	|- ( ( T. /\ ( A e. _V /\ B e. _V /\ C e. _V ) ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
8	5 7	mpan	|- ( ( A e. _V /\ B e. _V /\ C e. _V ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
9	1 2 3 8	mp3an	|- ( ( A F B ) F C ) = ( A F ( B F C ) )