Step | Hyp | Ref
| Expression |
1 | | bnj1312.5 |
. . 3
     |
2 | | bnj1312.6 |
. . . 4
 
   |
3 | 2 | simplbi 460 |
. . . . . . 7

  |
4 | 1 | bnj21 32058 |
. . . . . . . 8
 |
5 | 4 | a1i 11 |
. . . . . . 7

  |
6 | 2 | simprbi 464 |
. . . . . . 7

  |
7 | 1 | bnj1230 32148 |
. . . . . . . 8
 
  |
8 | 7 | bnj1228 32354 |
. . . . . . 7
 
 

    |
9 | 3, 5, 6, 8 | syl3anc 1219 |
. . . . . 6
  
    |
10 | | bnj1312.7 |
. . . . . 6
  
     |
11 | | nfv 1674 |
. . . . . . . . 9
  |
12 | 7 | nfcii 2606 |
. . . . . . . . . 10
   |
13 | | nfcv 2616 |
. . . . . . . . . 10
   |
14 | 12, 13 | nfne 2783 |
. . . . . . . . 9
  |
15 | 11, 14 | nfan 1866 |
. . . . . . . 8
  
  |
16 | 2, 15 | nfxfr 1616 |
. . . . . . 7
   |
17 | 16 | nfri 1813 |
. . . . . 6
     |
18 | 9, 10, 17 | bnj1521 32196 |
. . . . 5
     |
19 | 10 | simp2bi 1004 |
. . . . 5

  |
20 | 1 | bnj1538 32200 |
. . . . . 6
     |
21 | | bnj1312.1 |
. . . . . . . . 9
 
         |
22 | | bnj1312.2 |
. . . . . . . . 9
           |
23 | | bnj1312.3 |
. . . . . . . . 9
 
             |
24 | | bnj1312.4 |
. . . . . . . . 9
 
            |
25 | | bnj1312.8 |
. . . . . . . . 9
   ![]. ].](_drbrack.gif)   |
26 | | bnj1312.9 |
. . . . . . . . 9
 
       |
27 | | bnj1312.10 |
. . . . . . . . 9
  |
28 | | bnj1312.11 |
. . . . . . . . 9
           |
29 | | bnj1312.12 |
. . . . . . . . 9
            |
30 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29 | bnj1489 32399 |
. . . . . . . 8

  |
31 | | bnj1312.13 |
. . . . . . . . . . 11
           |
32 | | bnj1312.14 |
. . . . . . . . . . 11
          |
33 | 10, 3 | bnj835 32104 |
. . . . . . . . . . . . . 14

  |
34 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27 | bnj1384 32375 |
. . . . . . . . . . . . . 14

  |
35 | 33, 34 | syl 16 |
. . . . . . . . . . . . 13
   |
36 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27 | bnj1415 32381 |
. . . . . . . . . . . . 13
        |
37 | 35, 36 | bnj1422 32183 |
. . . . . . . . . . . 12

       |
38 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 36 | bnj1416 32382 |
. . . . . . . . . . . . . 14
            |
39 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 35, 38, 36 | bnj1421 32385 |
. . . . . . . . . . . . 13
   |
40 | 39, 38 | bnj1422 32183 |
. . . . . . . . . . . 12

           |
41 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 31, 32, 37, 40 | bnj1423 32394 |
. . . . . . . . . . 11
            |
42 | 32 | fneq2i 5617 |
. . . . . . . . . . . 12

           |
43 | 40, 42 | sylibr 212 |
. . . . . . . . . . 11

  |
44 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 31, 32 | bnj1452 32395 |
. . . . . . . . . . 11

  |
45 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 31, 32, 30, 41, 43, 44 | bnj1463 32398 |
. . . . . . . . . 10

  |
46 | 45, 38 | jca 532 |
. . . . . . . . 9
              |
47 | 21, 22, 23, 24, 1, 2, 10, 25, 26, 27, 28, 29, 46 | bnj1491 32400 |
. . . . . . . 8
                  |
48 | 30, 47 | mpdan 668 |
. . . . . . 7
   
            |
49 | 48, 24 | bnj1198 32141 |
. . . . . 6
     |
50 | 20, 49 | nsyl3 119 |
. . . . 5
   |
51 | 18, 19, 50 | bnj1304 32165 |
. . . 4
 |
52 | 2, 51 | bnj1541 32201 |
. . 3

  |
53 | 1, 52 | bnj1476 32192 |
. 2


    |
54 | 24 | exbii 1635 |
. . . 4
  
               |
55 | | df-rex 2805 |
. . . 4
 
        
               |
56 | 54, 55 | bitr4i 252 |
. . 3
  

           |
57 | 56 | ralbii 2839 |
. 2
 
 
 
           |
58 | 53, 57 | sylib 196 |
1



           |