Step | Hyp | Ref
| Expression |
1 | | cA |
. . . 4
class ๐ด |
2 | | cc 11108 |
. . . 4
class
โ |
3 | 1, 2 | wcel 2107 |
. . 3
wff ๐ด โ โ |
4 | | cB |
. . . 4
class ๐ต |
5 | | chba 30172 |
. . . 4
class
โ |
6 | 4, 5 | wcel 2107 |
. . 3
wff ๐ต โ โ |
7 | | cC |
. . . 4
class ๐ถ |
8 | 7, 5 | wcel 2107 |
. . 3
wff ๐ถ โ โ |
9 | 3, 6, 8 | w3a 1088 |
. 2
wff (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ
โ) |
10 | | cva 30173 |
. . . . 5
class
+โ |
11 | 4, 7, 10 | co 7409 |
. . . 4
class (๐ต +โ ๐ถ) |
12 | | csm 30174 |
. . . 4
class
ยทโ |
13 | 1, 11, 12 | co 7409 |
. . 3
class (๐ด
ยทโ (๐ต +โ ๐ถ)) |
14 | 1, 4, 12 | co 7409 |
. . . 4
class (๐ด
ยทโ ๐ต) |
15 | 1, 7, 12 | co 7409 |
. . . 4
class (๐ด
ยทโ ๐ถ) |
16 | 14, 15, 10 | co 7409 |
. . 3
class ((๐ด
ยทโ ๐ต) +โ (๐ด ยทโ ๐ถ)) |
17 | 13, 16 | wceq 1542 |
. 2
wff (๐ด
ยทโ (๐ต +โ ๐ถ)) = ((๐ด ยทโ ๐ต) +โ (๐ด
ยทโ ๐ถ)) |
18 | 9, 17 | wi 4 |
1
wff ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด
ยทโ (๐ต +โ ๐ถ)) = ((๐ด ยทโ ๐ต) +โ (๐ด
ยทโ ๐ถ))) |