Proof of Theorem xordidc
Step | Hyp | Ref
| Expression |
1 | | dcbi 938 |
. . . . 5
DECID DECID DECID 
    |
2 | 1 | imp 124 |
. . . 4
 DECID DECID 
DECID 
   |
3 | | annimdc 939 |
. . . . . 6
DECID DECID    
  
 
      |
4 | 3 | imp 124 |
. . . . 5
 DECID DECID      
 
 
     |
5 | | pm5.32 453 |
. . . . . 6
  
    
     |
6 | 5 | notbii 669 |
. . . . 5
    
 
 
    |
7 | 4, 6 | bitrdi 196 |
. . . 4
 DECID DECID      
 
  
      |
8 | 2, 7 | sylan2 286 |
. . 3
 DECID DECID
DECID     
 
  
      |
9 | | xornbidc 1402 |
. . . . . 6
DECID DECID   
      |
10 | 9 | imp 124 |
. . . . 5
 DECID DECID 
 
 
    |
11 | 10 | adantl 277 |
. . . 4
 DECID DECID
DECID     
     |
12 | 11 | anbi2d 464 |
. . 3
 DECID DECID
DECID     
   
     |
13 | | dcan 935 |
. . . . 5
 DECID DECID  DECID 
   |
14 | 13 | adantrr 479 |
. . . 4
 DECID DECID
DECID   DECID     |
15 | | dcan 935 |
. . . . 5
 DECID DECID  DECID 
   |
16 | 15 | adantrl 478 |
. . . 4
 DECID DECID
DECID   DECID     |
17 | | xornbidc 1402 |
. . . 4
DECID   DECID            
       |
18 | 14, 16, 17 | sylc 62 |
. . 3
 DECID DECID
DECID            
      |
19 | 8, 12, 18 | 3bitr4d 220 |
. 2
 DECID DECID
DECID     
           |
20 | 19 | exp32 365 |
1
DECID DECID DECID
    
           |