Step | Hyp | Ref
| Expression |
1 | | bnj1145.1 |
. . 3
        
   |
2 | | bnj1145.2 |
. . 3
  
    
            |
3 | | bnj1145.3 |
. . 3
     |
4 | | bnj1145.4 |
. . 3
 
    |
5 | 1, 2, 3, 4 | bnj882 29785 |
. 2
  
  
       |
6 | | ss2iun 4307 |
. . . 4
 
            
   |
7 | | bnj1145.5 |
. . . . . . 7
 
   |
8 | 7, 4 | bnj1083 29835 |
. . . . . 6

    |
9 | 2 | bnj1095 29641 |
. . . . . . . . 9
     |
10 | 9, 7 | bnj1096 29642 |
. . . . . . . 8
     |
11 | 3 | bnj1098 29643 |
. . . . . . . . . . . . . . . . 17
   


   |
12 | 7 | bnj1232 29663 |
. . . . . . . . . . . . . . . . . 18

  |
13 | 12 | 3anim3i 1202 |
. . . . . . . . . . . . . . . . 17
 
 
   |
14 | 11, 13 | bnj1101 29644 |
. . . . . . . . . . . . . . . 16
     
   |
15 | | ancl 553 |
. . . . . . . . . . . . . . . 16
  
 
      
 
     |
16 | 14, 15 | bnj101 29577 |
. . . . . . . . . . . . . . 15
      
 
    |
17 | | bnj1145.6 |
. . . . . . . . . . . . . . . . 17
  
 
    |
18 | 17 | imbi2i 318 |
. . . . . . . . . . . . . . . 16
  
 
 
    
     |
19 | 18 | exbii 1728 |
. . . . . . . . . . . . . . 15
      
      
 
     |
20 | 16, 19 | mpbir 214 |
. . . . . . . . . . . . . 14
       |
21 | | bnj213 29741 |
. . . . . . . . . . . . . . . 16
      |
22 | 21 | bnj226 29590 |
. . . . . . . . . . . . . . 15
           |
23 | | simpr 467 |
. . . . . . . . . . . . . . . . . . 19
 
   |
24 | 17, 23 | bnj833 29617 |
. . . . . . . . . . . . . . . . . 18

  |
25 | | simp2 1015 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
26 | 12 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
27 | 3 | bnj923 29627 |
. . . . . . . . . . . . . . . . . . . . 21
   |
28 | | elnn 6728 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
29 | 27, 28 | sylan2 481 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
30 | 25, 26, 29 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . 19
 
   |
31 | 17, 30 | bnj832 29616 |
. . . . . . . . . . . . . . . . . 18

  |
32 | | vex 3059 |
. . . . . . . . . . . . . . . . . . . 20
 |
33 | 32 | bnj216 29588 |
. . . . . . . . . . . . . . . . . . 19
   |
34 | | elnn 6728 |
. . . . . . . . . . . . . . . . . . 19
 
   |
35 | 33, 34 | sylan 478 |
. . . . . . . . . . . . . . . . . 18
 
   |
36 | 24, 31, 35 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17

  |
37 | 17, 25 | bnj832 29616 |
. . . . . . . . . . . . . . . . . 18

  |
38 | 24, 37 | eqeltrrd 2540 |
. . . . . . . . . . . . . . . . 17
   |
39 | 2 | bnj589 29768 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    
            |
40 | 39 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . 22
       
            |
41 | 40 | bnj708 29614 |
. . . . . . . . . . . . . . . . . . . . 21
 
  
  
              |
42 | | rsp 2765 |
. . . . . . . . . . . . . . . . . . . . 21
 

    
           
                  |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
       
             |
44 | 7, 43 | sylbi 200 |
. . . . . . . . . . . . . . . . . . 19
  
                  |
45 | 44 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . . 18
 
  
                  |
46 | 17, 45 | bnj832 29616 |
. . . . . . . . . . . . . . . . 17
  
                  |
47 | 36, 38, 46 | mp2d 46 |
. . . . . . . . . . . . . . . 16
     
           |
48 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . 18
       
   |
49 | 48 | eqeq1d 2463 |
. . . . . . . . . . . . . . . . 17
      
        
                 |
50 | 24, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
      
        
                 |
51 | 47, 50 | mpbird 240 |
. . . . . . . . . . . . . . 15
                 |
52 | 22, 51 | bnj1262 29670 |
. . . . . . . . . . . . . 14
    
  |
53 | 20, 52 | bnj1023 29640 |
. . . . . . . . . . . . 13
           |
54 | | 3anass 995 |
. . . . . . . . . . . . . . 15
 
       |
55 | 54 | imbi1i 331 |
. . . . . . . . . . . . . 14
  
    
             |
56 | 55 | exbii 1728 |
. . . . . . . . . . . . 13
         
               |
57 | 53, 56 | mpbi 213 |
. . . . . . . . . . . 12
      
      |
58 | 1 | biimpi 199 |
. . . . . . . . . . . . . . 15
        
   |
59 | 7, 58 | bnj771 29623 |
. . . . . . . . . . . . . 14
        
   |
60 | | fveq2 5887 |
. . . . . . . . . . . . . . 15

          |
61 | | bnj213 29741 |
. . . . . . . . . . . . . . . 16
  
   |
62 | | sseq1 3464 |
. . . . . . . . . . . . . . . 16
        
     
    
   |
63 | 61, 62 | mpbiri 241 |
. . . . . . . . . . . . . . 15
        
       |
64 | | sseq1 3464 |
. . . . . . . . . . . . . . . 16
        
        
   |
65 | 64 | biimpar 492 |
. . . . . . . . . . . . . . 15
                     |
66 | 60, 63, 65 | syl2an 484 |
. . . . . . . . . . . . . 14
         
 
      |
67 | 59, 66 | sylan2 481 |
. . . . . . . . . . . . 13
         |
68 | 67 | adantrl 727 |
. . . . . . . . . . . 12
           |
69 | 57, 68 | bnj1109 29646 |
. . . . . . . . . . 11
        
  |
70 | | 19.9v 1822 |
. . . . . . . . . . 11
                     |
71 | 69, 70 | mpbi 213 |
. . . . . . . . . 10
  
      |
72 | 71 | expcom 441 |
. . . . . . . . 9
     
   |
73 | | fndm 5696 |
. . . . . . . . . . 11

  |
74 | 7, 73 | bnj770 29622 |
. . . . . . . . . 10
   |
75 | | eleq2 2528 |
. . . . . . . . . . 11
     |
76 | 75 | imbi1d 323 |
. . . . . . . . . 10
       

        |
77 | 74, 76 | syl 17 |
. . . . . . . . 9
       

        |
78 | 72, 77 | mpbird 240 |
. . . . . . . 8
         |
79 | 10, 78 | hbralrimi 2795 |
. . . . . . 7
         |
80 | 79 | exlimiv 1786 |
. . . . . 6
           |
81 | 8, 80 | sylbi 200 |
. . . . 5
         |
82 | | ss2iun 4307 |
. . . . . 6
 
              |
83 | | bnj1143 29650 |
. . . . . 6
  |
84 | 82, 83 | syl6ss 3455 |
. . . . 5
 
             |
85 | 81, 84 | syl 17 |
. . . 4
         |
86 | 6, 85 | mprg 2762 |
. . 3

        |
87 | 4 | bnj1317 29681 |
. . . 4
 
  |
88 | 87 | bnj1146 29651 |
. . 3

 |
89 | 86, 88 | sstri 3452 |
. 2

       |
90 | 5, 89 | eqsstri 3473 |
1
  
   |