Metamath Proof Explorer


Theorem caovdir

Description: Reverse distributive law. (Contributed by NM, 26-Aug-1995)

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

Proof

Step Hyp Ref Expression
1 caovdir.1
 |-  A e. _V
2 caovdir.2
 |-  B e. _V
3 caovdir.3
 |-  C e. _V
4 caovdir.com
 |-  ( x G y ) = ( y G x )
5 caovdir.distr
 |-  ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) )
6 3 1 2 5 caovdi
 |-  ( C G ( A F B ) ) = ( ( C G A ) F ( C G B ) )
7 ovex
 |-  ( A F B ) e. _V
8 3 7 4 caovcom
 |-  ( C G ( A F B ) ) = ( ( A F B ) G C )
9 3 1 4 caovcom
 |-  ( C G A ) = ( A G C )
10 3 2 4 caovcom
 |-  ( C G B ) = ( B G C )
11 9 10 oveq12i
 |-  ( ( C G A ) F ( C G B ) ) = ( ( A G C ) F ( B G C ) )
12 6 8 11 3eqtr3i
 |-  ( ( A F B ) G C ) = ( ( A G C ) F ( B G C ) )