Proof of Theorem bnj607
Step | Hyp | Ref
| Expression |
1 | | bnj607.37 |
. . . . 5
 
       |
2 | 1 | anim1i 578 |
. . . 4
         
   |
3 | | nfv 1769 |
. . . . . . 7
   |
4 | 3 | 19.41 2070 |
. . . . . 6
           |
5 | 4 | exbii 1726 |
. . . . 5
               |
6 | | bnj607.5 |
. . . . . . . 8
   
 ![]. ].](_drbrack.gif)    |
7 | 6 | bnj1095 29665 |
. . . . . . 7
     |
8 | 7 | nfi 1682 |
. . . . . 6
   |
9 | 8 | 19.41 2070 |
. . . . 5
      
        |
10 | 5, 9 | bitr2i 258 |
. . . 4
      
        |
11 | 2, 10 | sylib 201 |
. . 3
             |
12 | | bnj607.19 |
. . . . . . . . . 10
 
   |
13 | 12 | bnj1232 29687 |
. . . . . . . . 9

  |
14 | | bnj219 29613 |
. . . . . . . . . 10

  |
15 | 12, 14 | bnj770 29646 |
. . . . . . . . 9

  |
16 | 13, 15 | jca 541 |
. . . . . . . 8
 
   |
17 | 16 | anim1i 578 |
. . . . . . 7
         |
18 | | bnj170 29575 |
. . . . . . 7
  
 
    |
19 | 17, 18 | sylibr 217 |
. . . . . 6
   
   |
20 | | bnj607.38 |
. . . . . 6
     |
21 | 19, 20 | syl 17 |
. . . . 5
     |
22 | | simpl 464 |
. . . . 5
     |
23 | 21, 22 | jca 541 |
. . . 4
       |
24 | 23 | 2eximi 1716 |
. . 3
               |
25 | | bnj607.31 |
. . . . . . . . . . . 12
  

       |
26 | 25 | biimpi 199 |
. . . . . . . . . . 11
   
       |
27 | | euex 2343 |
. . . . . . . . . . 11
           |
28 | 26, 27 | syl6 33 |
. . . . . . . . . 10
   
       |
29 | 28 | impcom 437 |
. . . . . . . . 9
  

       |
30 | | bnj607.17 |
. . . . . . . . 9
     |
31 | 29, 30 | bnj1198 29679 |
. . . . . . . 8
  

     |
32 | 31 | adantrr 731 |
. . . . . . 7
  

       |
33 | | id 22 |
. . . . . . . . . . 11
 
     |
34 | 33 | 3com23 1237 |
. . . . . . . . . 10
 
     |
35 | 34 | 3expia 1233 |
. . . . . . . . 9
 

      |
36 | 35 | eximdv 1772 |
. . . . . . . 8
 

          |
37 | 36 | ad2ant2rl 763 |
. . . . . . 7
  

             |
38 | 32, 37 | mpd 15 |
. . . . . 6
  

         |
39 | | bnj607.41 |
. . . . . . . 8
 

  |
40 | | bnj607.42 |
. . . . . . . 8
 
   |
41 | | bnj607.43 |
. . . . . . . 8
 
   |
42 | 39, 40, 41 | 3jca 1210 |
. . . . . . 7
 
     |
43 | 42 | eximi 1715 |
. . . . . 6
           |
44 | | nfe1 1935 |
. . . . . . 7
       |
45 | | bnj607.28 |
. . . . . . . . 9
 |
46 | | nfcv 2612 |
. . . . . . . . . 10
   |
47 | | nfv 1769 |
. . . . . . . . . . 11

 |
48 | | bnj607.300 |
. . . . . . . . . . . 12
   ![]. ].](_drbrack.gif)   |
49 | | nfsbc1v 3275 |
. . . . . . . . . . . 12
  
 ![]. ].](_drbrack.gif)  |
50 | 48, 49 | nfxfr 1704 |
. . . . . . . . . . 11
   |
51 | | bnj607.301 |
. . . . . . . . . . . 12
   ![]. ].](_drbrack.gif)   |
52 | | nfsbc1v 3275 |
. . . . . . . . . . . 12
  
 ![]. ].](_drbrack.gif)  |
53 | 51, 52 | nfxfr 1704 |
. . . . . . . . . . 11
   |
54 | 47, 50, 53 | nf3an 2033 |
. . . . . . . . . 10
     |
55 | | fneq1 5674 |
. . . . . . . . . . 11
 
   |
56 | | sbceq1a 3266 |
. . . . . . . . . . . 12
    ![]. ].](_drbrack.gif)    |
57 | 56, 48 | syl6bbr 271 |
. . . . . . . . . . 11
     |
58 | | sbceq1a 3266 |
. . . . . . . . . . . 12
    ![]. ].](_drbrack.gif)    |
59 | 58, 51 | syl6bbr 271 |
. . . . . . . . . . 11
     |
60 | 55, 57, 59 | 3anbi123d 1365 |
. . . . . . . . . 10
         |
61 | 46, 54, 60 | spcegf 3116 |
. . . . . . . . 9
           |
62 | 45, 61 | ax-mp 5 |
. . . . . . . 8
         |
63 | | bnj607.32 |
. . . . . . . . . . . 12

           |
64 | | bnj607.400 |
. . . . . . . . . . . . . 14
   ![]. ].](_drbrack.gif)   |
65 | | bnj607.1 |
. . . . . . . . . . . . . 14
            |
66 | 64, 65 | bnj154 29761 |
. . . . . . . . . . . . 13
            |
67 | 66, 48, 45 | bnj526 29771 |
. . . . . . . . . . . 12
            |
68 | 63, 67 | bitr4i 260 |
. . . . . . . . . . 11

  |
69 | | bnj607.33 |
. . . . . . . . . . . 12

 
  
              |
70 | | bnj607.2 |
. . . . . . . . . . . . . 14
  
    
            |
71 | | bnj607.401 |
. . . . . . . . . . . . . 14
   ![]. ].](_drbrack.gif)   |
72 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
73 | 70, 71, 72 | bnj540 29775 |
. . . . . . . . . . . . 13
 

    
            |
74 | 73, 51, 45 | bnj540 29775 |
. . . . . . . . . . . 12
 

    
            |
75 | 69, 74 | bitr4i 260 |
. . . . . . . . . . 11

  |
76 | 68, 75 | anbi12i 711 |
. . . . . . . . . 10
  
    |
77 | 76 | anbi2i 708 |
. . . . . . . . 9
  
 

     |
78 | | 3anass 1011 |
. . . . . . . . 9
         |
79 | | 3anass 1011 |
. . . . . . . . 9
  

     |
80 | 77, 78, 79 | 3bitr4i 285 |
. . . . . . . 8
   
   |
81 | | nfv 1769 |
. . . . . . . . 9
     |
82 | | nfv 1769 |
. . . . . . . . . 10
  |
83 | | nfsbc1v 3275 |
. . . . . . . . . . 11
    ![]. ].](_drbrack.gif)  |
84 | 64, 83 | nfxfr 1704 |
. . . . . . . . . 10
   |
85 | | nfsbc1v 3275 |
. . . . . . . . . . 11
    ![]. ].](_drbrack.gif)  |
86 | 71, 85 | nfxfr 1704 |
. . . . . . . . . 10
   |
87 | 82, 84, 86 | nf3an 2033 |
. . . . . . . . 9
     |
88 | | fneq1 5674 |
. . . . . . . . . 10
 
   |
89 | | sbceq1a 3266 |
. . . . . . . . . . 11
    ![]. ].](_drbrack.gif)    |
90 | 89, 64 | syl6bbr 271 |
. . . . . . . . . 10
     |
91 | | sbceq1a 3266 |
. . . . . . . . . . 11
    ![]. ].](_drbrack.gif)    |
92 | 91, 71 | syl6bbr 271 |
. . . . . . . . . 10
     |
93 | 88, 90, 92 | 3anbi123d 1365 |
. . . . . . . . 9
         |
94 | 81, 87, 93 | cbvex 2128 |
. . . . . . . 8
    
      |
95 | 62, 80, 94 | 3imtr4i 274 |
. . . . . . 7
  
      |
96 | 44, 95 | exlimi 2015 |
. . . . . 6
           |
97 | 38, 43, 96 | 3syl 18 |
. . . . 5
  

         |
98 | 97 | expcom 442 |
. . . 4
     
       |
99 | 98 | exlimivv 1786 |
. . 3
         
       |
100 | 11, 24, 99 | 3syl 18 |
. 2
       
       |
101 | 100 | 3impa 1226 |
1
 

          |