Proof of Theorem bnj1417
Step | Hyp | Ref
| Expression |
1 | | bnj1417.1 |
. . . 4
   |
2 | 1 | biimpi 199 |
. . 3

  |
3 | | bnj1417.4 |
. . . . . 6
 
   |
4 | | bnj1418 29921 |
. . . . . . . . . . 11
          |
5 | 4 | adantl 473 |
. . . . . . . . . 10
       
    |
6 | 3, 2 | bnj835 29642 |
. . . . . . . . . . . 12

  |
7 | | df-bnj15 29570 |
. . . . . . . . . . . . 13

    |
8 | 7 | simplbi 467 |
. . . . . . . . . . . 12

  |
9 | 6, 8 | syl 17 |
. . . . . . . . . . 11

  |
10 | | bnj213 29765 |
. . . . . . . . . . . 12
      |
11 | 10 | sseli 3414 |
. . . . . . . . . . 11
        |
12 | | frirr 4816 |
. . . . . . . . . . 11
 
     |
13 | 9, 11, 12 | syl2an 485 |
. . . . . . . . . 10
       
    |
14 | 5, 13 | pm2.65da 586 |
. . . . . . . . 9
        |
15 | | nfv 1769 |
. . . . . . . . . . . . . 14
   |
16 | | nfv 1769 |
. . . . . . . . . . . . . 14
  |
17 | | bnj1417.3 |
. . . . . . . . . . . . . . . 16
     
 ![]. ].](_drbrack.gif)    |
18 | 17 | bnj1095 29665 |
. . . . . . . . . . . . . . 15
     |
19 | 18 | nfi 1682 |
. . . . . . . . . . . . . 14
   |
20 | 15, 16, 19 | nf3an 2033 |
. . . . . . . . . . . . 13
  
  |
21 | 3, 20 | nfxfr 1704 |
. . . . . . . . . . . 12
   |
22 | 6 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
              
  |
23 | | simplr 770 |
. . . . . . . . . . . . . . . . 17
              
       |
24 | 10, 23 | sseldi 3416 |
. . . . . . . . . . . . . . . 16
              
  |
25 | | simpr 468 |
. . . . . . . . . . . . . . . 16
              
       |
26 | | bnj1125 29873 |
. . . . . . . . . . . . . . . 16
 
                  |
27 | 22, 24, 25, 26 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
              
    
       |
28 | | bnj1147 29875 |
. . . . . . . . . . . . . . . . . 18
      |
29 | 28, 25 | sseldi 3416 |
. . . . . . . . . . . . . . . . 17
              
  |
30 | | bnj906 29813 |
. . . . . . . . . . . . . . . . 17
 
             |
31 | 22, 29, 30 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
              
    
       |
32 | 31, 23 | sseldd 3419 |
. . . . . . . . . . . . . . 15
              
       |
33 | 27, 32 | sseldd 3419 |
. . . . . . . . . . . . . 14
              
       |
34 | 17 | biimpi 199 |
. . . . . . . . . . . . . . . . . 18
       ![]. ].](_drbrack.gif)    |
35 | 3, 34 | bnj837 29644 |
. . . . . . . . . . . . . . . . 17
       ![]. ].](_drbrack.gif)    |
36 | 35 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
              

  
  ![]. ].](_drbrack.gif)    |
37 | | bnj1418 29921 |
. . . . . . . . . . . . . . . . 17
          |
38 | 37 | ad2antlr 741 |
. . . . . . . . . . . . . . . 16
              
    |
39 | | rsp 2773 |
. . . . . . . . . . . . . . . 16
 
   
 ![]. ].](_drbrack.gif)        ![]. ].](_drbrack.gif)     |
40 | 36, 24, 38, 39 | syl3c 62 |
. . . . . . . . . . . . . . 15
              
  ![]. ].](_drbrack.gif)   |
41 | | vex 3034 |
. . . . . . . . . . . . . . . 16
 |
42 | | bnj1417.2 |
. . . . . . . . . . . . . . . . 17
        |
43 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . 19
      
        |
44 | | bnj1318 29906 |
. . . . . . . . . . . . . . . . . . . 20
             |
45 | 44 | eleq2d 2534 |
. . . . . . . . . . . . . . . . . . 19
      
        |
46 | 43, 45 | bitrd 261 |
. . . . . . . . . . . . . . . . . 18
      
        |
47 | 46 | notbid 301 |
. . . . . . . . . . . . . . . . 17
 
    
        |
48 | 42, 47 | syl5bb 265 |
. . . . . . . . . . . . . . . 16
          |
49 | 41, 48 | sbcie 3290 |
. . . . . . . . . . . . . . 15
   ![]. ].](_drbrack.gif)        |
50 | 40, 49 | sylib 201 |
. . . . . . . . . . . . . 14
              
       |
51 | 33, 50 | pm2.65da 586 |
. . . . . . . . . . . . 13
       
       |
52 | 51 | ex 441 |
. . . . . . . . . . . 12
      
        |
53 | 21, 52 | ralrimi 2800 |
. . . . . . . . . . 11
             |
54 | | ralnex 2834 |
. . . . . . . . . . 11
 
                      |
55 | 53, 54 | sylib 201 |
. . . . . . . . . 10
              |
56 | | eliun 4274 |
. . . . . . . . . 10
           
            |
57 | 55, 56 | sylnibr 312 |
. . . . . . . . 9
 
           |
58 | | ioran 498 |
. . . . . . . . 9
                 

    
             |
59 | 14, 57, 58 | sylanbrc 677 |
. . . . . . . 8
       
            |
60 | 3 | simp2bi 1046 |
. . . . . . . . . . 11

  |
61 | | bnj1417.5 |
. . . . . . . . . . . 12
                 |
62 | 61 | bnj1414 29918 |
. . . . . . . . . . 11
 
        |
63 | 6, 60, 62 | syl2anc 673 |
. . . . . . . . . 10
        |
64 | 63 | eleq2d 2534 |
. . . . . . . . 9
      
   |
65 | 61 | bnj1138 29672 |
. . . . . . . . 9

      
            |
66 | 64, 65 | syl6bb 269 |
. . . . . . . 8
      
      
             |
67 | 59, 66 | mtbird 308 |
. . . . . . 7
        |
68 | 67, 42 | sylibr 217 |
. . . . . 6
   |
69 | 3, 68 | sylbir 218 |
. . . . 5
 
   |
70 | 69 | 3exp 1230 |
. . . 4
       |
71 | 70 | ralrimiv 2808 |
. . 3
  
   |
72 | 17 | bnj1204 29893 |
. . 3
 
 
 

  |
73 | 2, 71, 72 | syl2anc 673 |
. 2
    |
74 | 42 | ralbii 2823 |
. 2
 

       |
75 | 73, 74 | sylib 201 |
1
 
       |