Step |
Hyp |
Ref |
Expression |
0 |
|
cA |
โข ๐ด |
1 |
|
cc |
โข โ |
2 |
0 1
|
wcel |
โข ๐ด โ โ |
3 |
|
cB |
โข ๐ต |
4 |
3 1
|
wcel |
โข ๐ต โ โ |
5 |
|
cC |
โข ๐ถ |
6 |
5 1
|
wcel |
โข ๐ถ โ โ |
7 |
2 4 6
|
w3a |
โข ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) |
8 |
|
cmul |
โข ยท |
9 |
0 3 8
|
co |
โข ( ๐ด ยท ๐ต ) |
10 |
9 5 8
|
co |
โข ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) |
11 |
3 5 8
|
co |
โข ( ๐ต ยท ๐ถ ) |
12 |
0 11 8
|
co |
โข ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) |
13 |
10 12
|
wceq |
โข ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) |
14 |
7 13
|
wi |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) ) |