Step |
Hyp |
Ref |
Expression |
1 |
|
caov.1 |
|- A e. _V |
2 |
|
caov.2 |
|- B e. _V |
3 |
|
caov.3 |
|- C e. _V |
4 |
|
caov.com |
|- ( x F y ) = ( y F x ) |
5 |
|
caov.ass |
|- ( ( x F y ) F z ) = ( x F ( y F z ) ) |
6 |
1 3 2 5
|
caovass |
|- ( ( A F C ) F B ) = ( A F ( C F B ) ) |
7 |
1 3 2 4 5
|
caov12 |
|- ( A F ( C F B ) ) = ( C F ( A F B ) ) |
8 |
6 7
|
eqtri |
|- ( ( A F C ) F B ) = ( C F ( A F B ) ) |
9 |
1 2 3 4 5
|
caov32 |
|- ( ( A F B ) F C ) = ( ( A F C ) F B ) |
10 |
3 1 2 4 5
|
caov32 |
|- ( ( C F A ) F B ) = ( ( C F B ) F A ) |
11 |
3 1 2 5
|
caovass |
|- ( ( C F A ) F B ) = ( C F ( A F B ) ) |
12 |
10 11
|
eqtr3i |
|- ( ( C F B ) F A ) = ( C F ( A F B ) ) |
13 |
8 9 12
|
3eqtr4i |
|- ( ( A F B ) F C ) = ( ( C F B ) F A ) |