Proof of Theorem pm4.55dc
Step | Hyp | Ref
| Expression |
1 | | pm4.54dc 902 |
. . . . 5
DECID DECID   
      |
2 | 1 | imp 124 |
. . . 4
 DECID DECID   
      |
3 | | dcn 842 |
. . . . . . . . 9
DECID DECID   |
4 | 3 | anim2i 342 |
. . . . . . . 8
 DECID DECID  DECID
DECID    |
5 | | dcor 935 |
. . . . . . . . 9
DECID DECID DECID 
    |
6 | 5 | imp 124 |
. . . . . . . 8
 DECID DECID 
DECID     |
7 | 4, 6 | syl 14 |
. . . . . . 7
 DECID DECID  DECID 
   |
8 | | dcn 842 |
. . . . . . . . 9
DECID DECID   |
9 | | dcan2 934 |
. . . . . . . . 9
DECID DECID
DECID      |
10 | 8, 9 | syl 14 |
. . . . . . . 8
DECID DECID DECID 
    |
11 | 10 | imp 124 |
. . . . . . 7
 DECID DECID  DECID     |
12 | 7, 11 | jca 306 |
. . . . . 6
 DECID DECID  DECID  
DECID      |
13 | | con2bidc 875 |
. . . . . . 7
DECID   DECID  
   
  
          |
14 | 13 | imp 124 |
. . . . . 6
 DECID 
 DECID 
     
    
       |
15 | 12, 14 | syl 14 |
. . . . 5
 DECID DECID    
   
         |
16 | 15 | biimprd 158 |
. . . 4
 DECID DECID    
     

      |
17 | 2, 16 | mpd 13 |
. . 3
 DECID DECID    
     |
18 | 17 | bicomd 141 |
. 2
 DECID DECID     
    |
19 | 18 | ex 115 |
1
DECID DECID  
 
     |