Step | Hyp | Ref
| Expression |
1 | | rexeq 2673 |
. . 3

      |
2 | 1 | dcbid 838 |
. 2

DECID 
DECID     |
3 | | rexeq 2673 |
. . 3
  
    |
4 | 3 | dcbid 838 |
. 2
 DECID 
DECID 
   |
5 | | rexeq 2673 |
. . 3
      
         |
6 | 5 | dcbid 838 |
. 2
     DECID  DECID          |
7 | | rexeq 2673 |
. . 3
  
    |
8 | 7 | dcbid 838 |
. 2
 DECID 
DECID 
   |
9 | | rex0 3440 |
. . . . 5

 |
10 | 9 | olci 732 |
. . . 4
     |
11 | | df-dc 835 |
. . . 4
DECID 
 
    |
12 | 10, 11 | mpbir 146 |
. . 3
DECID   |
13 | 12 | a1i 9 |
. 2
   DECID  DECID    |
14 | | simpr 110 |
. . . . . . . . 9
       DECID 
      DECID

   ![] ]](rbrack.gif) 
  ![] ]](rbrack.gif)   |
15 | | sbsbc 2966 |
. . . . . . . . . 10
   ![] ]](rbrack.gif)   ![]. ].](_drbrack.gif)   |
16 | | rexsns 3630 |
. . . . . . . . . 10
    
  ![]. ].](_drbrack.gif)   |
17 | 15, 16 | bitr4i 187 |
. . . . . . . . 9
   ![] ]](rbrack.gif)       |
18 | 14, 17 | sylib 122 |
. . . . . . . 8
       DECID 
      DECID

   ![] ]](rbrack.gif) 
      |
19 | 18 | olcd 734 |
. . . . . . 7
       DECID 
      DECID

   ![] ]](rbrack.gif) 
         |
20 | | rexun 3315 |
. . . . . . 7
      
 
       |
21 | 19, 20 | sylibr 134 |
. . . . . 6
       DECID 
      DECID

   ![] ]](rbrack.gif) 
        |
22 | 21 | orcd 733 |
. . . . 5
       DECID 
      DECID

   ![] ]](rbrack.gif) 
                |
23 | | df-dc 835 |
. . . . 5
DECID                       |
24 | 22, 23 | sylibr 134 |
. . . 4
       DECID 
      DECID

   ![] ]](rbrack.gif) 
DECID         |
25 | | simpr 110 |
. . . . . . . . 9
        DECID 
      DECID

   ![] ]](rbrack.gif)  
    |
26 | 25 | orcd 733 |
. . . . . . . 8
        DECID 
      DECID

   ![] ]](rbrack.gif)  
  

      |
27 | 26, 20 | sylibr 134 |
. . . . . . 7
        DECID 
      DECID

   ![] ]](rbrack.gif)  
         |
28 | 27 | orcd 733 |
. . . . . 6
        DECID 
      DECID

   ![] ]](rbrack.gif)  
                 |
29 | 28, 23 | sylibr 134 |
. . . . 5
        DECID 
      DECID

   ![] ]](rbrack.gif)  
 DECID 
       |
30 | | simpr 110 |
. . . . . . . . 9
        DECID 
      DECID

   ![] ]](rbrack.gif)   

  |
31 | | simpr 110 |
. . . . . . . . . . 11
       DECID 
      DECID

   ![] ]](rbrack.gif)    ![] ]](rbrack.gif)   |
32 | 17 | notbii 668 |
. . . . . . . . . . 11
   ![] ]](rbrack.gif)
      |
33 | 31, 32 | sylib 122 |
. . . . . . . . . 10
       DECID 
      DECID

   ![] ]](rbrack.gif)        |
34 | 33 | adantr 276 |
. . . . . . . . 9
        DECID 
      DECID

   ![] ]](rbrack.gif)   
      |
35 | | ioran 752 |
. . . . . . . . 9
   
   
         |
36 | 30, 34, 35 | sylanbrc 417 |
. . . . . . . 8
        DECID 
      DECID

   ![] ]](rbrack.gif)   
 
       |
37 | 20 | notbii 668 |
. . . . . . . 8
      
 
       |
38 | 36, 37 | sylibr 134 |
. . . . . . 7
        DECID 
      DECID

   ![] ]](rbrack.gif)   
        |
39 | 38 | olcd 734 |
. . . . . 6
        DECID 
      DECID

   ![] ]](rbrack.gif)                    |
40 | 39, 23 | sylibr 134 |
. . . . 5
        DECID 
      DECID

   ![] ]](rbrack.gif)    DECID 
       |
41 | | exmiddc 836 |
. . . . . 6
DECID 
 

   |
42 | 41 | ad2antlr 489 |
. . . . 5
       DECID 
      DECID

   ![] ]](rbrack.gif)   

   |
43 | 29, 40, 42 | mpjaodan 798 |
. . . 4
       DECID 
      DECID

   ![] ]](rbrack.gif) 
DECID         |
44 | | simplrr 536 |
. . . . . . 7
     
DECID

 
   
DECID       |
45 | 44 | eldifad 3140 |
. . . . . 6
     
DECID

 
   
DECID     |
46 | | simp-4r 542 |
. . . . . 6
     
DECID

 
   
DECID   
DECID   |
47 | | nfs1v 1939 |
. . . . . . . 8
    ![] ]](rbrack.gif)  |
48 | 47 | nfdc 1659 |
. . . . . . 7
 DECID   ![] ]](rbrack.gif)  |
49 | | sbequ12 1771 |
. . . . . . . 8
    ![] ]](rbrack.gif)    |
50 | 49 | dcbid 838 |
. . . . . . 7
 DECID
DECID   ![] ]](rbrack.gif)    |
51 | 48, 50 | rspc 2835 |
. . . . . 6
  
DECID DECID   ![] ]](rbrack.gif)    |
52 | 45, 46, 51 | sylc 62 |
. . . . 5
     
DECID

 
   
DECID  
DECID   ![] ]](rbrack.gif)   |
53 | | exmiddc 836 |
. . . . 5
DECID   ![] ]](rbrack.gif)    ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
54 | 52, 53 | syl 14 |
. . . 4
     
DECID

 
   
DECID      ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
55 | 24, 43, 54 | mpjaodan 798 |
. . 3
     
DECID

 
   
DECID  
DECID         |
56 | 55 | ex 115 |
. 2
   

DECID   
    DECID  DECID 
        |
57 | | simpl 109 |
. 2
   DECID    |
58 | 2, 4, 6, 8, 13, 56, 57 | findcard2sd 6885 |
1
   DECID  DECID    |