Theorem caovdi

Description: Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995) (Revised by Mario Carneiro, 28-Jun-2013)

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

Proof

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