Proof of Theorem bnj1445
Step | Hyp | Ref
| Expression |
1 | | bnj1445.21 |
. 2
                   |
2 | | bnj1445.20 |
. . . . 5
     |
3 | | bnj1445.19 |
. . . . . . 7
          |
4 | | bnj1445.17 |
. . . . . . . . 9
     |
5 | | bnj1445.7 |
. . . . . . . . . . . . 13
  
     |
6 | | bnj1445.6 |
. . . . . . . . . . . . . . 15
 
   |
7 | | nfv 1769 |
. . . . . . . . . . . . . . . 16

 |
8 | | bnj1445.5 |
. . . . . . . . . . . . . . . . . 18
     |
9 | | bnj1445.4 |
. . . . . . . . . . . . . . . . . . . . . 22
 
            |
10 | | bnj1445.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
             |
11 | | nfre1 2846 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
12 | 11 | nfab 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
             |
13 | 10, 12 | nfcxfr 2610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
14 | 13 | nfcri 2606 |
. . . . . . . . . . . . . . . . . . . . . . 23
  |
15 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . . . 23
            |
16 | 14, 15 | nfan 2031 |
. . . . . . . . . . . . . . . . . . . . . 22
              |
17 | 9, 16 | nfxfr 1704 |
. . . . . . . . . . . . . . . . . . . . 21
   |
18 | 17 | nfex 2050 |
. . . . . . . . . . . . . . . . . . . 20
     |
19 | 18 | nfn 2003 |
. . . . . . . . . . . . . . . . . . 19
    |
20 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
   |
21 | 19, 20 | nfrab 2958 |
. . . . . . . . . . . . . . . . . 18
  
    |
22 | 8, 21 | nfcxfr 2610 |
. . . . . . . . . . . . . . . . 17
   |
23 | | nfcv 2612 |
. . . . . . . . . . . . . . . . 17
   |
24 | 22, 23 | nfne 2742 |
. . . . . . . . . . . . . . . 16
  |
25 | 7, 24 | nfan 2031 |
. . . . . . . . . . . . . . 15
  
  |
26 | 6, 25 | nfxfr 1704 |
. . . . . . . . . . . . . 14
   |
27 | 22 | nfcri 2606 |
. . . . . . . . . . . . . 14
  |
28 | | nfv 1769 |
. . . . . . . . . . . . . . 15
    |
29 | 22, 28 | nfral 2789 |
. . . . . . . . . . . . . 14
      |
30 | 26, 27, 29 | nf3an 2033 |
. . . . . . . . . . . . 13
  

    |
31 | 5, 30 | nfxfr 1704 |
. . . . . . . . . . . 12
   |
32 | 31 | nfri 1972 |
. . . . . . . . . . 11
     |
33 | 32 | bnj1351 29710 |
. . . . . . . . . 10
         |
34 | 33 | nfi 1682 |
. . . . . . . . 9
     |
35 | 4, 34 | nfxfr 1704 |
. . . . . . . 8
   |
36 | | nfv 1769 |
. . . . . . . 8
       |
37 | 35, 36 | nfan 2031 |
. . . . . . 7
          |
38 | 3, 37 | nfxfr 1704 |
. . . . . 6
   |
39 | | bnj1445.9 |
. . . . . . . 8
 
       |
40 | | nfcv 2612 |
. . . . . . . . . 10
       |
41 | | bnj1445.8 |
. . . . . . . . . . 11
   ![]. ].](_drbrack.gif)   |
42 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
43 | 42, 17 | nfsbc 3277 |
. . . . . . . . . . 11
    ![]. ].](_drbrack.gif)  |
44 | 41, 43 | nfxfr 1704 |
. . . . . . . . . 10
   |
45 | 40, 44 | nfrex 2848 |
. . . . . . . . 9
         |
46 | 45 | nfab 2616 |
. . . . . . . 8
   
       |
47 | 39, 46 | nfcxfr 2610 |
. . . . . . 7
   |
48 | 47 | nfcri 2606 |
. . . . . 6
  |
49 | | nfv 1769 |
. . . . . 6
  |
50 | 38, 48, 49 | nf3an 2033 |
. . . . 5
  
  |
51 | 2, 50 | nfxfr 1704 |
. . . 4
   |
52 | 51 | nfri 1972 |
. . 3
     |
53 | | ax-5 1766 |
. . 3
              |
54 | 14 | nfri 1972 |
. . 3
    |
55 | | ax-5 1766 |
. . 3
                       |
56 | 52, 53, 54, 55 | bnj982 29662 |
. 2
                        
            |
57 | 1, 56 | hbxfrbi 1702 |
1
     |