Step | Hyp | Ref
| Expression |
1 | | bnj849.10 |
. 2
 
   |
2 | | bnj849.1 |
. . . 4
        
   |
3 | | bnj849.2 |
. . . 4
  
    
            |
4 | | bnj849.3 |
. . . 4
     |
5 | | bnj849.5 |
. . . 4
 
   |
6 | | bnj849.6 |
. . . 4
     |
7 | 2, 3, 4, 5, 6 | bnj865 29740 |
. . 3
        |
8 | | bnj849.4 |
. . . . . . . 8
 
    |
9 | | bnj849.7 |
. . . . . . . 8
   ![]. ].](_drbrack.gif)   |
10 | | bnj849.8 |
. . . . . . . 8
   ![]. ].](_drbrack.gif)   |
11 | 8, 9, 10 | bnj873 29741 |
. . . . . . 7
 
    |
12 | | df-rex 2743 |
. . . . . . . . 9
   
        |
13 | | 19.29 1739 |
. . . . . . . . . . 11
      
          

        |
14 | | an12 811 |
. . . . . . . . . . . . 13
   
                 |
15 | | df-3an 988 |
. . . . . . . . . . . . . . . 16
 
  

   |
16 | 1 | anbi1i 706 |
. . . . . . . . . . . . . . . 16
  
      |
17 | 15, 5, 16 | 3bitr4i 285 |
. . . . . . . . . . . . . . 15
     |
18 | | id 22 |
. . . . . . . . . . . . . . . . 17
   |
19 | | bnj849.9 |
. . . . . . . . . . . . . . . . . . . 20

  ![]. ].](_drbrack.gif)   |
20 | 6, 9, 10, 19 | bnj581 29725 |
. . . . . . . . . . . . . . . . . . . 20


   |
21 | 19, 20 | bitr3i 259 |
. . . . . . . . . . . . . . . . . . 19
   ![]. ].](_drbrack.gif)     |
22 | 2, 3, 4, 5, 6 | bnj864 29739 |
. . . . . . . . . . . . . . . . . . . 20
     |
23 | | df-rex 2743 |
. . . . . . . . . . . . . . . . . . . . 21
        |
24 | | exancom 1726 |
. . . . . . . . . . . . . . . . . . . . 21
       
   |
25 | 23, 24 | sylbb 202 |
. . . . . . . . . . . . . . . . . . . 20
        |
26 | | nfeu1 2310 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
27 | | nfe1 1922 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
28 | 26, 27 | nfan 2016 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
29 | | nfsbc1v 3255 |
. . . . . . . . . . . . . . . . . . . . . . 23
    ![]. ].](_drbrack.gif)  |
30 | | nfv 1765 |
. . . . . . . . . . . . . . . . . . . . . . 23
  |
31 | 29, 30 | nfim 2008 |
. . . . . . . . . . . . . . . . . . . . . 22
     ![]. ].](_drbrack.gif)   |
32 | 28, 31 | nfim 2008 |
. . . . . . . . . . . . . . . . . . . . 21
              ![]. ].](_drbrack.gif)
   |
33 | | sbceq1a 3246 |
. . . . . . . . . . . . . . . . . . . . . . 23
    ![]. ].](_drbrack.gif)    |
34 | | elequ1 1898 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
35 | 33, 34 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . 22
   
   ![]. ].](_drbrack.gif)     |
36 | 35 | imbi2d 322 |
. . . . . . . . . . . . . . . . . . . . 21
             
      
 
   ![]. ].](_drbrack.gif)      |
37 | | eupick 2366 |
. . . . . . . . . . . . . . . . . . . . 21
      
 
    |
38 | 32, 36, 37 | chvar 2107 |
. . . . . . . . . . . . . . . . . . . 20
      
 
   ![]. ].](_drbrack.gif)    |
39 | 22, 25, 38 | syl2an 484 |
. . . . . . . . . . . . . . . . . . 19
  
    ![]. ].](_drbrack.gif)    |
40 | 21, 39 | syl5bir 226 |
. . . . . . . . . . . . . . . . . 18
  
       |
41 | 40 | ex 440 |
. . . . . . . . . . . . . . . . 17
          |
42 | 18, 41 | embantd 56 |
. . . . . . . . . . . . . . . 16
            |
43 | 42 | impd 437 |
. . . . . . . . . . . . . . 15
     
      |
44 | 17, 43 | sylbir 218 |
. . . . . . . . . . . . . 14
              |
45 | 44 | expimpd 612 |
. . . . . . . . . . . . 13
    

        |
46 | 14, 45 | syl5bi 225 |
. . . . . . . . . . . 12
     
        |
47 | 46 | exlimdv 1783 |
. . . . . . . . . . 11
      
         |
48 | 13, 47 | syl5 33 |
. . . . . . . . . 10
      
           |
49 | 48 | expdimp 443 |
. . . . . . . . 9
     
 
          |
50 | 12, 49 | syl5bi 225 |
. . . . . . . 8
     
 
 
     |
51 | 50 | abssdv 3471 |
. . . . . . 7
     
 
       |
52 | 11, 51 | syl5eqss 3444 |
. . . . . 6
     
 
  |
53 | | vex 3016 |
. . . . . . 7
 |
54 | 53 | ssex 4519 |
. . . . . 6
   |
55 | 52, 54 | syl 17 |
. . . . 5
     
 
  |
56 | 55 | ex 440 |
. . . 4
    

    |
57 | 56 | exlimdv 1783 |
. . 3
            |
58 | 7, 57 | mpi 20 |
. 2

  |
59 | 1, 58 | sylbir 218 |
1
 
   |