Proof of Theorem bilukdc
Step | Hyp | Ref
| Expression |
1 | | bicom 138 |
. . . . . 6
  
    |
2 | 1 | bibi1i 226 |
. . . . 5
  
        |
3 | | biassdc 1327 |
. . . . . 6
DECID DECID DECID
  

  
       |
4 | 3 | imp31 252 |
. . . . 5
  DECID
DECID  DECID
     
       |
5 | 2, 4 | syl5bb 190 |
. . . 4
  DECID
DECID  DECID
     
       |
6 | 5 | ancom1s 534 |
. . 3
  DECID
DECID  DECID
     
       |
7 | | dcbi 878 |
. . . . . 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 878 |
. . . . . 6
DECID DECID DECID      |
12 | | dcbi 878 |
. . . . . 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 1327 |
. . . 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 497 |
. . 3
  DECID
DECID  DECID
 DECID   |
19 | 11 | imp 122 |
. . . 4
 DECID DECID  DECID 
   |
20 | 19 | adantlr 461 |
. . 3
  DECID
DECID  DECID
 DECID     |
21 | | biassdc 1327 |
. . 3
DECID DECID DECID 
     
  
          |
22 | 10, 18, 20, 21 | syl3c 62 |
. 2
  DECID
DECID  DECID
     
  
        |
23 | 17, 22 | bitr4d 189 |
1
  DECID
DECID  DECID
  
  
       |