Proof of Theorem bilukdc
Step | Hyp | Ref
| Expression |
1 | | bicom 138 |
. . . . . 6
|
2 | 1 | bibi1i 226 |
. . . . 5
|
3 | | biassdc 1326 |
. . . . . 6
DECID DECID DECID
|
4 | 3 | imp31 252 |
. . . . 5
DECID
DECID DECID
|
5 | 2, 4 | syl5bb 190 |
. . . 4
DECID
DECID DECID
|
6 | 5 | ancom1s 533 |
. . 3
DECID
DECID DECID
|
7 | | dcbi 877 |
. . . . . 6
DECID DECID DECID |
8 | 7 | imp 122 |
. . . . 5
DECID DECID DECID
|
9 | 8 | adantr 270 |
. . . 4
DECID
DECID DECID
DECID |
10 | | simpr 108 |
. . . 4
DECID
DECID DECID
DECID |
11 | | dcbi 877 |
. . . . . 6
DECID DECID DECID |
12 | | dcbi 877 |
. . . . . 6
DECID DECID
DECID
|
13 | 11, 12 | syl9 71 |
. . . . 5
DECID DECID DECID
DECID
|
14 | 13 | imp31 252 |
. . . 4
DECID
DECID DECID
DECID
|
15 | | biassdc 1326 |
. . . 4
DECID
DECID
DECID
|
16 | 9, 10, 14, 15 | syl3c 62 |
. . 3
DECID
DECID DECID
|
17 | 6, 16 | mpbid 145 |
. 2
DECID
DECID DECID
|
18 | | simplr 496 |
. . 3
DECID
DECID DECID
DECID |
19 | 11 | imp 122 |
. . . 4
DECID DECID DECID
|
20 | 19 | adantlr 460 |
. . 3
DECID
DECID DECID
DECID |
21 | | biassdc 1326 |
. . 3
DECID DECID DECID
|
22 | 10, 18, 20, 21 | syl3c 62 |
. 2
DECID
DECID DECID
|
23 | 17, 22 | bitr4d 189 |
1
DECID
DECID DECID
|