Proof of Theorem bnj1489
Step | Hyp | Ref
| Expression |
1 | | bnj1489.12 |
. 2
            |
2 | | bnj1489.10 |
. . . 4
  |
3 | | bnj1489.7 |
. . . . . . . 8
  
     |
4 | | bnj1489.6 |
. . . . . . . . 9
 
   |
5 | | bnj1364 29909 |
. . . . . . . . . 10

  |
6 | | df-bnj13 29568 |
. . . . . . . . . 10


       |
7 | 5, 6 | sylib 201 |
. . . . . . . . 9


       |
8 | 4, 7 | bnj832 29640 |
. . . . . . . 8
         |
9 | 3, 8 | bnj835 29642 |
. . . . . . 7
         |
10 | | bnj1489.5 |
. . . . . . . 8
     |
11 | 10, 3 | bnj1212 29683 |
. . . . . . 7

  |
12 | 9, 11 | bnj1294 29701 |
. . . . . 6
        |
13 | | nfv 1769 |
. . . . . . . . 9
   |
14 | | nfv 1769 |
. . . . . . . . 9
  |
15 | | nfra1 2785 |
. . . . . . . . 9
      |
16 | 13, 14, 15 | nf3an 2033 |
. . . . . . . 8
  

    |
17 | 3, 16 | nfxfr 1704 |
. . . . . . 7
   |
18 | 4 | simplbi 467 |
. . . . . . . . . . 11

  |
19 | 3, 18 | bnj835 29642 |
. . . . . . . . . 10

  |
20 | 19 | adantr 472 |
. . . . . . . . 9
       
  |
21 | | bnj1489.1 |
. . . . . . . . . . 11
 
         |
22 | | bnj1489.2 |
. . . . . . . . . . 11
           |
23 | | bnj1489.3 |
. . . . . . . . . . 11
 
             |
24 | | bnj1489.4 |
. . . . . . . . . . 11
 
            |
25 | | bnj1489.8 |
. . . . . . . . . . 11
   ![]. ].](_drbrack.gif)   |
26 | 21, 22, 23, 24, 10, 4, 3, 25 | bnj1388 29914 |
. . . . . . . . . 10
           |
27 | 26 | r19.21bi 2776 |
. . . . . . . . 9
       
    |
28 | | nfv 1769 |
. . . . . . . . . . . 12
  |
29 | | nfsbc1v 3275 |
. . . . . . . . . . . . . 14
  
 ![]. ].](_drbrack.gif)  |
30 | 25, 29 | nfxfr 1704 |
. . . . . . . . . . . . 13
   |
31 | 30 | nfex 2050 |
. . . . . . . . . . . 12
     |
32 | 28, 31 | nfan 2031 |
. . . . . . . . . . 11
       |
33 | 30 | nfeu 2335 |
. . . . . . . . . . 11
     |
34 | 32, 33 | nfim 2023 |
. . . . . . . . . 10
           |
35 | | sneq 3969 |
. . . . . . . . . . . . . . . . 17
  
    |
36 | | bnj1318 29906 |
. . . . . . . . . . . . . . . . 17
             |
37 | 35, 36 | uneq12d 3580 |
. . . . . . . . . . . . . . . 16
                     |
38 | 37 | eqeq2d 2481 |
. . . . . . . . . . . . . . 15
 
        
            |
39 | 38 | anbi2d 718 |
. . . . . . . . . . . . . 14
                           |
40 | 21, 22, 23, 24, 25 | bnj1373 29911 |
. . . . . . . . . . . . . 14
 
            |
41 | 39, 40 | syl6bbr 271 |
. . . . . . . . . . . . 13
                |
42 | 41 | exbidv 1776 |
. . . . . . . . . . . 12
       
      
     |
43 | 42 | anbi2d 718 |
. . . . . . . . . . 11
     
                  |
44 | 41 | eubidv 2339 |
. . . . . . . . . . 11
       
      
     |
45 | 43, 44 | imbi12d 327 |
. . . . . . . . . 10
      
          
               
  
      |
46 | | biid 244 |
. . . . . . . . . . 11
 
                       |
47 | 21, 22, 23, 46 | bnj1321 29908 |
. . . . . . . . . 10
 
     
          
            |
48 | 34, 45, 47 | chvar 2119 |
. . . . . . . . 9
 
       |
49 | 20, 27, 48 | syl2anc 673 |
. . . . . . . 8
       
    |
50 | 49 | ex 441 |
. . . . . . 7
            |
51 | 17, 50 | ralrimi 2800 |
. . . . . 6
           |
52 | | bnj1489.9 |
. . . . . . 7
 
       |
53 | 52 | a1i 11 |
. . . . . 6

          |
54 | | biid 244 |
. . . . . . 7
      
               
                        |
55 | 54 | bnj1366 29713 |
. . . . . 6
      
                  |
56 | 12, 51, 53, 55 | syl3anc 1292 |
. . . . 5

  |
57 | | uniexg 6607 |
. . . . 5
    |
58 | 56, 57 | syl 17 |
. . . 4
    |
59 | 2, 58 | syl5eqel 2553 |
. . 3

  |
60 | | snex 4641 |
. . . 4
          |
61 | 60 | a1i 11 |
. . 3
            |
62 | 59, 61 | bnj1149 29676 |
. 2
              |
63 | 1, 62 | syl5eqel 2553 |
1

  |