Proof of Theorem pm4.55dc
Step | Hyp | Ref
| Expression |
1 | | pm4.54dc 804 |
. . . . 5
DECID DECID          |
2 | 1 | imp 115 |
. . . 4
 DECID DECID          |
3 | | dcn 745 |
. . . . . . . . 9
DECID DECID   |
4 | 3 | anim2i 324 |
. . . . . . . 8
 DECID DECID  DECID DECID    |
5 | | dcor 842 |
. . . . . . . . 9
DECID DECID
DECID      |
6 | 5 | imp 115 |
. . . . . . . 8
 DECID DECID 
DECID     |
7 | 4, 6 | syl 14 |
. . . . . . 7
 DECID DECID  DECID     |
8 | | dcn 745 |
. . . . . . . . 9
DECID DECID   |
9 | | dcan 841 |
. . . . . . . . 9
DECID DECID DECID      |
10 | 8, 9 | syl 14 |
. . . . . . . 8
DECID DECID DECID      |
11 | 10 | imp 115 |
. . . . . . 7
 DECID DECID  DECID     |
12 | 7, 11 | jca 290 |
. . . . . 6
 DECID DECID  DECID  
DECID      |
13 | | con2bidc 768 |
. . . . . . 7
DECID   DECID                    |
14 | 13 | imp 115 |
. . . . . 6
 DECID   DECID   
   
     
      |
15 | 12, 14 | syl 14 |
. . . . 5
 DECID DECID                  |
16 | 15 | biimprd 147 |
. . . 4
 DECID DECID           
      |
17 | 2, 16 | mpd 13 |
. . 3
 DECID DECID          |
18 | 17 | bicomd 129 |
. 2
 DECID DECID          |
19 | 18 | ex 108 |
1
DECID DECID          |