Step |
Hyp |
Ref |
Expression |
1 |
|
caovdir.1 |
⊢ 𝐴 ∈ V |
2 |
|
caovdir.2 |
⊢ 𝐵 ∈ V |
3 |
|
caovdir.3 |
⊢ 𝐶 ∈ V |
4 |
|
caovdir.com |
⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) |
5 |
|
caovdir.distr |
⊢ ( 𝑥 𝐺 ( 𝑦 𝐹 𝑧 ) ) = ( ( 𝑥 𝐺 𝑦 ) 𝐹 ( 𝑥 𝐺 𝑧 ) ) |
6 |
3 1 2 5
|
caovdi |
⊢ ( 𝐶 𝐺 ( 𝐴 𝐹 𝐵 ) ) = ( ( 𝐶 𝐺 𝐴 ) 𝐹 ( 𝐶 𝐺 𝐵 ) ) |
7 |
|
ovex |
⊢ ( 𝐴 𝐹 𝐵 ) ∈ V |
8 |
3 7 4
|
caovcom |
⊢ ( 𝐶 𝐺 ( 𝐴 𝐹 𝐵 ) ) = ( ( 𝐴 𝐹 𝐵 ) 𝐺 𝐶 ) |
9 |
3 1 4
|
caovcom |
⊢ ( 𝐶 𝐺 𝐴 ) = ( 𝐴 𝐺 𝐶 ) |
10 |
3 2 4
|
caovcom |
⊢ ( 𝐶 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐶 ) |
11 |
9 10
|
oveq12i |
⊢ ( ( 𝐶 𝐺 𝐴 ) 𝐹 ( 𝐶 𝐺 𝐵 ) ) = ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐶 ) ) |
12 |
6 8 11
|
3eqtr3i |
⊢ ( ( 𝐴 𝐹 𝐵 ) 𝐺 𝐶 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐶 ) ) |