Proof of Theorem xordidc
Step | Hyp | Ref
| Expression |
1 | | dcbi 877 |
. . . . 5
DECID DECID DECID
|
2 | 1 | imp 122 |
. . . 4
DECID DECID
DECID
|
3 | | annimdc 878 |
. . . . . 6
DECID DECID
|
4 | 3 | imp 122 |
. . . . 5
DECID DECID
|
5 | | pm5.32 440 |
. . . . . 6
|
6 | 5 | notbii 626 |
. . . . 5
|
7 | 4, 6 | syl6bb 194 |
. . . 4
DECID DECID
|
8 | 2, 7 | sylan2 280 |
. . 3
DECID DECID
DECID
|
9 | | xornbidc 1322 |
. . . . . 6
DECID DECID
|
10 | 9 | imp 122 |
. . . . 5
DECID DECID
|
11 | 10 | adantl 271 |
. . . 4
DECID DECID
DECID
|
12 | 11 | anbi2d 451 |
. . 3
DECID DECID
DECID
|
13 | | dcan 875 |
. . . . . 6
DECID DECID DECID |
14 | 13 | imp 122 |
. . . . 5
DECID DECID DECID
|
15 | 14 | adantrr 462 |
. . . 4
DECID DECID
DECID DECID |
16 | | dcan 875 |
. . . . . 6
DECID DECID DECID |
17 | 16 | imp 122 |
. . . . 5
DECID DECID DECID
|
18 | 17 | adantrl 461 |
. . . 4
DECID DECID
DECID DECID |
19 | | xornbidc 1322 |
. . . 4
DECID DECID
|
20 | 15, 18, 19 | sylc 61 |
. . 3
DECID DECID
DECID
|
21 | 8, 12, 20 | 3bitr4d 218 |
. 2
DECID DECID
DECID
|
22 | 21 | exp32 357 |
1
DECID DECID DECID
|