Proof of Theorem dn1dc
Step | Hyp | Ref
| Expression |
1 | | pm2.45 656 |
. . . . 5
     |
2 | | imnan 623 |
. . . . 5
   
       |
3 | 1, 2 | mpbi 133 |
. . . 4
     |
4 | 3 | biorfi 664 |
. . 3
         |
5 | | orcom 646 |
. . 3
               |
6 | | ordir 729 |
. . 3
          
      |
7 | 4, 5, 6 | 3bitri 195 |
. 2
           |
8 | | pm4.45 697 |
. . . . . 6
       |
9 | | simprrl 491 |
. . . . . . 7
 DECID DECID DECID DECID    DECID   |
10 | | dcor 842 |
. . . . . . . . 9
DECID DECID DECID      |
11 | 10 | imp 115 |
. . . . . . . 8
 DECID DECID 
DECID     |
12 | 11 | ad2antll 460 |
. . . . . . 7
 DECID DECID DECID DECID    DECID     |
13 | | anordc 862 |
. . . . . . 7
DECID DECID                |
14 | 9, 12, 13 | sylc 56 |
. . . . . 6
 DECID DECID DECID DECID                |
15 | 8, 14 | syl5bb 181 |
. . . . 5
 DECID DECID DECID DECID            |
16 | 15 | orbi2d 703 |
. . . 4
 DECID DECID DECID DECID                |
17 | 16 | anbi2d 437 |
. . 3
 DECID DECID DECID DECID         
       
          |
18 | | dcor 842 |
. . . . . . . 8
DECID DECID DECID      |
19 | | dcn 745 |
. . . . . . . 8
DECID   DECID
    |
20 | 18, 19 | syl6 29 |
. . . . . . 7
DECID DECID DECID      |
21 | 20 | imp 115 |
. . . . . 6
 DECID DECID  DECID     |
22 | 21 | adantrr 448 |
. . . . 5
 DECID DECID DECID DECID    DECID     |
23 | | dcor 842 |
. . . . 5
DECID   DECID DECID        |
24 | 22, 9, 23 | sylc 56 |
. . . 4
 DECID DECID DECID DECID    DECID       |
25 | | dcn 745 |
. . . . . . . 8
DECID DECID   |
26 | 9, 25 | syl 14 |
. . . . . . 7
 DECID DECID DECID DECID    DECID   |
27 | | dcn 745 |
. . . . . . . 8
DECID   DECID
    |
28 | 12, 27 | syl 14 |
. . . . . . 7
 DECID DECID DECID DECID    DECID     |
29 | | dcor 842 |
. . . . . . 7
DECID DECID   DECID        |
30 | 26, 28, 29 | sylc 56 |
. . . . . 6
 DECID DECID DECID DECID    DECID       |
31 | | dcn 745 |
. . . . . 6
DECID     DECID       |
32 | 30, 31 | syl 14 |
. . . . 5
 DECID DECID DECID DECID    DECID       |
33 | | dcor 842 |
. . . . . 6
DECID DECID    
DECID          |
34 | 33 | imp 115 |
. . . . 5
 DECID DECID     
DECID         |
35 | 32, 34 | syldan 266 |
. . . 4
 DECID DECID DECID DECID    DECID         |
36 | | anordc 862 |
. . . 4
DECID     DECID                                    |
37 | 24, 35, 36 | sylc 56 |
. . 3
 DECID DECID DECID DECID         
                      |
38 | 17, 37 | bitrd 177 |
. 2
 DECID DECID DECID DECID         
                  |
39 | 7, 38 | syl5rbb 182 |
1
 DECID DECID DECID DECID                    |