Step |
Hyp |
Ref |
Expression |
1 |
|
caov.1 |
⊢ 𝐴 ∈ V |
2 |
|
caov.2 |
⊢ 𝐵 ∈ V |
3 |
|
caov.3 |
⊢ 𝐶 ∈ V |
4 |
|
caov.com |
⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) |
5 |
|
caov.ass |
⊢ ( ( 𝑥 𝐹 𝑦 ) 𝐹 𝑧 ) = ( 𝑥 𝐹 ( 𝑦 𝐹 𝑧 ) ) |
6 |
1 3 2 5
|
caovass |
⊢ ( ( 𝐴 𝐹 𝐶 ) 𝐹 𝐵 ) = ( 𝐴 𝐹 ( 𝐶 𝐹 𝐵 ) ) |
7 |
1 3 2 4 5
|
caov12 |
⊢ ( 𝐴 𝐹 ( 𝐶 𝐹 𝐵 ) ) = ( 𝐶 𝐹 ( 𝐴 𝐹 𝐵 ) ) |
8 |
6 7
|
eqtri |
⊢ ( ( 𝐴 𝐹 𝐶 ) 𝐹 𝐵 ) = ( 𝐶 𝐹 ( 𝐴 𝐹 𝐵 ) ) |
9 |
1 2 3 4 5
|
caov32 |
⊢ ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( ( 𝐴 𝐹 𝐶 ) 𝐹 𝐵 ) |
10 |
3 1 2 4 5
|
caov32 |
⊢ ( ( 𝐶 𝐹 𝐴 ) 𝐹 𝐵 ) = ( ( 𝐶 𝐹 𝐵 ) 𝐹 𝐴 ) |
11 |
3 1 2 5
|
caovass |
⊢ ( ( 𝐶 𝐹 𝐴 ) 𝐹 𝐵 ) = ( 𝐶 𝐹 ( 𝐴 𝐹 𝐵 ) ) |
12 |
10 11
|
eqtr3i |
⊢ ( ( 𝐶 𝐹 𝐵 ) 𝐹 𝐴 ) = ( 𝐶 𝐹 ( 𝐴 𝐹 𝐵 ) ) |
13 |
8 9 12
|
3eqtr4i |
⊢ ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( ( 𝐶 𝐹 𝐵 ) 𝐹 𝐴 ) |