Proof of Theorem ceqsex8v
Step | Hyp | Ref
| Expression |
1 | | 19.42vv 1907 |
. . . . . . 7
       
     
    
  
         
       |
2 | 1 | 2exbii 1583 |
. . . . . 6
           
 
 
 
    
      
 
 
       
     |
3 | | 19.42vv 1907 |
. . . . . 6
       
         
    
  
             
 
     |
4 | 2, 3 | bitri 240 |
. . . . 5
           
 
 
 
    
  
             
 
     |
5 | | 3anass 938 |
. . . . . . . 8
     
     
     
        
      |
6 | | df-3an 936 |
. . . . . . . . 9
  
        
     |
7 | 6 | anbi2i 675 |
. . . . . . . 8
     
     
     
        
      |
8 | 5, 7 | bitr4i 243 |
. . . . . . 7
     
     
     
     
       |
9 | 8 | 2exbii 1583 |
. . . . . 6
       
     
             
     
     |
10 | 9 | 2exbii 1583 |
. . . . 5
           
 
 
 
                 
     
     |
11 | | df-3an 936 |
. . . . 5
  
              
     
             
 
     |
12 | 4, 10, 11 | 3bitr4i 268 |
. . . 4
           
 
 
 
        
          
       |
13 | 12 | 2exbii 1583 |
. . 3
                 
     
          
          
       |
14 | 13 | 2exbii 1583 |
. 2
                     
     
              
          
       |
15 | | ceqsex8v.1 |
. . . 4
 |
16 | | ceqsex8v.2 |
. . . 4
 |
17 | | ceqsex8v.3 |
. . . 4
 |
18 | | ceqsex8v.4 |
. . . 4
 |
19 | | ceqsex8v.9 |
. . . . . 6
     |
20 | 19 | 3anbi3d 1258 |
. . . . 5
   
       
     |
21 | 20 | 4exbidv 1630 |
. . . 4
           
 
             
     |
22 | | ceqsex8v.10 |
. . . . . 6
     |
23 | 22 | 3anbi3d 1258 |
. . . . 5
   
       
     |
24 | 23 | 4exbidv 1630 |
. . . 4
           
 
             
     |
25 | | ceqsex8v.11 |
. . . . . 6
     |
26 | 25 | 3anbi3d 1258 |
. . . . 5
   
       
     |
27 | 26 | 4exbidv 1630 |
. . . 4
           
 
             
     |
28 | | ceqsex8v.12 |
. . . . . 6
     |
29 | 28 | 3anbi3d 1258 |
. . . . 5
   
       
     |
30 | 29 | 4exbidv 1630 |
. . . 4
           
 
             
     |
31 | 15, 16, 17, 18, 21, 24, 27, 30 | ceqsex4v 2898 |
. . 3
            
          
    
           
    |
32 | | ceqsex8v.5 |
. . . 4
 |
33 | | ceqsex8v.6 |
. . . 4
 |
34 | | ceqsex8v.7 |
. . . 4
 |
35 | | ceqsex8v.8 |
. . . 4
 |
36 | | ceqsex8v.13 |
. . . 4
     |
37 | | ceqsex8v.14 |
. . . 4
     |
38 | | ceqsex8v.15 |
. . . 4
     |
39 | | ceqsex8v.16 |
. . . 4
     |
40 | 32, 33, 34, 35, 36, 37, 38, 39 | ceqsex4v 2898 |
. . 3
            
    |
41 | 31, 40 | bitri 240 |
. 2
            
          
    
  |
42 | 14, 41 | bitri 240 |
1
                     
     
     |