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 ) ) |