Step | Hyp | Ref
| Expression |
1 | | cA |
. . . 4
class ๐ด |
2 | | cc 7808 |
. . . 4
class
โ |
3 | 1, 2 | wcel 2148 |
. . 3
wff ๐ด โ โ |
4 | | cB |
. . . 4
class ๐ต |
5 | 4, 2 | wcel 2148 |
. . 3
wff ๐ต โ โ |
6 | | cC |
. . . 4
class ๐ถ |
7 | 6, 2 | wcel 2148 |
. . 3
wff ๐ถ โ โ |
8 | 3, 5, 7 | w3a 978 |
. 2
wff (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ
โ) |
9 | | cmul 7815 |
. . . . 5
class
ยท |
10 | 1, 4, 9 | co 5874 |
. . . 4
class (๐ด ยท ๐ต) |
11 | 10, 6, 9 | co 5874 |
. . 3
class ((๐ด ยท ๐ต) ยท ๐ถ) |
12 | 4, 6, 9 | co 5874 |
. . . 4
class (๐ต ยท ๐ถ) |
13 | 1, 12, 9 | co 5874 |
. . 3
class (๐ด ยท (๐ต ยท ๐ถ)) |
14 | 11, 13 | wceq 1353 |
. 2
wff ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ)) |
15 | 8, 14 | wi 4 |
1
wff ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ))) |