Proof of Theorem 2sb5ndVD
Step | Hyp | Ref
| Expression |
1 | | ax6e2ndeq 36996 |
. 2
   
        |
2 | | anabs5 826 |
. . . 4
             
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)  
         ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
3 | | 2pm13.193 36989 |
. . . . . . . . 9
      ![] ]](rbrack.gif)   ![] ]](rbrack.gif)        |
4 | 3 | exbii 1726 |
. . . . . . . 8
        ![] ]](rbrack.gif)   ![] ]](rbrack.gif) 
        |
5 | | hbs1 2285 |
. . . . . . . . . . . . 13
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
6 | | idn1 37012 |
. . . . . . . . . . . . . 14
 
   |
7 | | axc11 2163 |
. . . . . . . . . . . . . 14
 
     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
8 | 6, 7 | e1a 37074 |
. . . . . . . . . . . . 13
 
     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
9 | | imim1 78 |
. . . . . . . . . . . . 13
    ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)        ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)     |
10 | 5, 8, 9 | e01 37138 |
. . . . . . . . . . . 12
 
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
11 | 10 | in1 37009 |
. . . . . . . . . . 11
 
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
12 | | hbs1 2285 |
. . . . . . . . . . . . . . 15
   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   |
13 | 12 | sbt 2268 |
. . . . . . . . . . . . . 14
  ![] ]](rbrack.gif)    ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   |
14 | | sbi1 2241 |
. . . . . . . . . . . . . 14
   ![] ]](rbrack.gif)    ![] ]](rbrack.gif)     ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)    |
15 | 13, 14 | e0a 37222 |
. . . . . . . . . . . . 13
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   |
16 | | idn1 37012 |
. . . . . . . . . . . . . . 15
    |
17 | | axc11n 2157 |
. . . . . . . . . . . . . . . 16
 
   |
18 | 17 | con3i 142 |
. . . . . . . . . . . . . . 15
 
   |
19 | 16, 18 | e1a 37074 |
. . . . . . . . . . . . . 14
    |
20 | | sbal2 2310 |
. . . . . . . . . . . . . 14
 
   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
21 | 19, 20 | e1a 37074 |
. . . . . . . . . . . . 13
    ![] ]](rbrack.gif)     ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
22 | | imbi2 331 |
. . . . . . . . . . . . . 14
    ![] ]](rbrack.gif)     ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)     |
23 | 22 | biimpcd 232 |
. . . . . . . . . . . . 13
    ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  ![] ]](rbrack.gif)     ![] ]](rbrack.gif)      ![] ]](rbrack.gif)     ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)     |
24 | 15, 21, 23 | e01 37138 |
. . . . . . . . . . . 12
    ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
25 | 24 | in1 37009 |
. . . . . . . . . . 11
 
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
26 | 11, 25 | pm2.61i 169 |
. . . . . . . . . 10
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
27 | 26 | nfi 1682 |
. . . . . . . . 9
    ![] ]](rbrack.gif)   ![] ]](rbrack.gif)  |
28 | 27 | 19.41 2070 |
. . . . . . . 8
        ![] ]](rbrack.gif)   ![] ]](rbrack.gif) 
       ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
29 | 4, 28 | bitr3i 259 |
. . . . . . 7
              ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
30 | 29 | exbii 1726 |
. . . . . 6
                  ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
31 | 5 | nfi 1682 |
. . . . . . 7
  
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)  |
32 | 31 | 19.41 2070 |
. . . . . 6
          ![] ]](rbrack.gif)   ![] ]](rbrack.gif)           ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
33 | 30, 32 | bitr2i 258 |
. . . . 5
          ![] ]](rbrack.gif)   ![] ]](rbrack.gif)            |
34 | 33 | anbi2i 708 |
. . . 4
             
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)  
                  |
35 | 2, 34 | bitr3i 259 |
. . 3
          ![] ]](rbrack.gif)   ![] ]](rbrack.gif)              
     |
36 | | pm5.32 648 |
. . 3
       
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)          
      
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif) 
                   |
37 | 35, 36 | mpbir 214 |
. 2
     
    ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
           |
38 | 1, 37 | sylbi 200 |
1
       ![] ]](rbrack.gif)   ![] ]](rbrack.gif)
           |