Proof of Theorem ac6s6
Step | Hyp | Ref
| Expression |
1 | | hbe1 1916 |
. . . . . 6
         |
2 | | iftrue 3886 |
. . . . . . 7
          
     |
3 | 2 | abeq2d 2561 |
. . . . . 6
           
    |
4 | 1, 3 | exbidh 1726 |
. . . . 5
    
       
      |
5 | 4 | ibir 246 |
. . . 4
           
   |
6 | | vex 3047 |
. . . . . 6
 |
7 | 6 | exiftru 1807 |
. . . . 5
  |
8 | 1 | hbn 1976 |
. . . . . 6
        |
9 | | iffalse 3889 |
. . . . . . 7
          
   |
10 | 9 | eleq2d 2513 |
. . . . . 6
           
    |
11 | 8, 10 | exbidh 1726 |
. . . . 5
         
        |
12 | 7, 11 | mpbiri 237 |
. . . 4
           
   |
13 | 5, 12 | pm2.61i 168 |
. . 3
        
  |
14 | 13 | rgenw 2748 |
. 2

        
  |
15 | | nfe1 1917 |
. . . 4
     |
16 | | ac6s6.1 |
. . . 4
   |
17 | 15, 16 | nfim 2002 |
. . 3
       |
18 | | ac6s6.2 |
. . 3
 |
19 | | ac6s6.3 |
. . . . . 6
         |
20 | | id 22 |
. . . . . . . . . . . . . . 15

  |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . 14
      
               
                   
          
   |
22 | | ax-1 6 |
. . . . . . . . . . . . . . . . . . 19
      
               
                   
          
      
 
            
                   
             |
23 | | tsim3 32367 |
. . . . . . . . . . . . . . . . . . . 20
      
               
                   
                    
                   
                  
 
            
                   
             |
24 | 23 | a1d 26 |
. . . . . . . . . . . . . . . . . . 19
      
               
                   
          
          
                   
                  
 
            
                   
              |
25 | 22, 24 | cnf2dd 32320 |
. . . . . . . . . . . . . . . . . 18
      
               
                   
          
            
                   
            |
26 | | tsim3 32367 |
. . . . . . . . . . . . . . . . . . 19
      
               
                   
                        
                       
                   
            |
27 | 26 | a1d 26 |
. . . . . . . . . . . . . . . . . 18
      
               
                   
          
                 
                    
                   
             |
28 | 25, 27 | cnf2dd 32320 |
. . . . . . . . . . . . . . . . 17
      
               
                   
          
                
           |
29 | | tsim2 32366 |
. . . . . . . . . . . . . . . . . 18
      
               
                   
                             
           |
30 | 29 | a1d 26 |
. . . . . . . . . . . . . . . . 17
      
               
                   
          
                   
            |
31 | 28, 30 | cnf2dd 32320 |
. . . . . . . . . . . . . . . 16
      
               
                   
          
     |
32 | | tsim2 32366 |
. . . . . . . . . . . . . . . . . 18
      
               
                   
                      
               
                   
            |
33 | 32 | a1d 26 |
. . . . . . . . . . . . . . . . 17
      
               
                   
          
            
               
                   
             |
34 | 25, 33 | cnf2dd 32320 |
. . . . . . . . . . . . . . . 16
      
               
                   
          
  
     
         |
35 | 31, 34 | mpdd 41 |
. . . . . . . . . . . . . . 15
      
               
                   
          
     
        |
36 | | tsbi4 32371 |
. . . . . . . . . . . . . . . 16
      
               
                   
                
   
      
        |
37 | 36 | a1d 26 |
. . . . . . . . . . . . . . 15
      
               
                   
          
 
       
          
      |
38 | 35, 37 | cnfn2dd 32322 |
. . . . . . . . . . . . . 14
      
               
                   
          

             |
39 | 21, 38 | cnf2dd 32320 |
. . . . . . . . . . . . 13
      
               
                   
          
    
       |
40 | | tsim3 32367 |
. . . . . . . . . . . . . . . . 17
      
               
                   
                     
                 
     
              |
41 | 40 | a1d 26 |
. . . . . . . . . . . . . . . 16
      
               
                   
          
           
                 
     
               |
42 | 28, 41 | cnf2dd 32320 |
. . . . . . . . . . . . . . 15
      
               
                   
          
             
          |
43 | | tsim3 32367 |
. . . . . . . . . . . . . . . 16
      
               
                   
                   
                   
          |
44 | 43 | a1d 26 |
. . . . . . . . . . . . . . 15
      
               
                   
          
         
                   
           |
45 | 42, 44 | cnf2dd 32320 |
. . . . . . . . . . . . . 14
      
               
                   
          
        
         |
46 | | tsbi2 32369 |
. . . . . . . . . . . . . . 15
      
               
                   
                   
              
         |
47 | 46 | a1d 26 |
. . . . . . . . . . . . . 14
      
               
                   
          
         
              
          |
48 | 45, 47 | cnf2dd 32320 |
. . . . . . . . . . . . 13
      
               
                   
          
     
   
  
     |
49 | 39, 48 | cnf1dd 32319 |
. . . . . . . . . . . 12
      
               
                   
          
  
    |
50 | | tsim2 32366 |
. . . . . . . . . . . . . . . . . . 19
      
               
                   
                         
             |
51 | 50 | a1d 26 |
. . . . . . . . . . . . . . . . . 18
      
               
                   
          
                  
           |
52 | 42, 51 | cnf2dd 32320 |
. . . . . . . . . . . . . . . . 17
      
               
                   
          
       |
53 | | simplim 155 |
. . . . . . . . . . . . . . . . 17
      
               
                   
               
    |
54 | 52, 53 | syld 45 |
. . . . . . . . . . . . . . . 16
      
               
                   
          
     |
55 | | tsbi3 32370 |
. . . . . . . . . . . . . . . . 17
      
               
                   
           

     |
56 | 55 | a1d 26 |
. . . . . . . . . . . . . . . 16
      
               
                   
          
   
     |
57 | 54, 56 | cnfn2dd 32322 |
. . . . . . . . . . . . . . 15
      
               
                   
          
     |
58 | 21, 57 | cnf1dd 32319 |
. . . . . . . . . . . . . 14
      
               
                   
          
   |
59 | | tsim1 32365 |
. . . . . . . . . . . . . . . 16
      
               
                   
                      |
60 | 59 | a1d 26 |
. . . . . . . . . . . . . . 15
      
               
                   
          
    
        |
61 | 60 | or32dd 32323 |
. . . . . . . . . . . . . 14
      
               
                   
          
             |
62 | 58, 61 | cnf2dd 32320 |
. . . . . . . . . . . . 13
      
               
                   
          
           |
63 | 31, 62 | cnfn1dd 32321 |
. . . . . . . . . . . 12
      
               
                   
          
       |
64 | 49, 63 | contrd 32326 |
. . . . . . . . . . 11
      
               
                   
            |
65 | 64 | a1d 26 |
. . . . . . . . . 10
      
               
                   
          
   |
66 | | ax-1 6 |
. . . . . . . . . . . . . . 15
      
               
                   
          
      
 
            
                   
             |
67 | 23 | a1d 26 |
. . . . . . . . . . . . . . 15
      
               
                   
          
          
                   
                  
 
            
                   
              |
68 | 66, 67 | cnf2dd 32320 |
. . . . . . . . . . . . . 14
      
               
                   
          
            
                   
            |
69 | 26 | a1d 26 |
. . . . . . . . . . . . . 14
      
               
                   
          
                 
                    
                   
             |
70 | 68, 69 | cnf2dd 32320 |
. . . . . . . . . . . . 13
      
               
                   
          
                
           |
71 | 29 | a1d 26 |
. . . . . . . . . . . . 13
      
               
                   
          
                   
            |
72 | 70, 71 | cnf2dd 32320 |
. . . . . . . . . . . 12
      
               
                   
          
     |
73 | 32 | a1d 26 |
. . . . . . . . . . . . 13
      
               
                   
          
            
               
                   
             |
74 | 68, 73 | cnf2dd 32320 |
. . . . . . . . . . . 12
      
               
                   
          
  
     
         |
75 | 72, 74 | mpdd 41 |
. . . . . . . . . . 11
      
               
                   
          
     
        |
76 | | tsbi3 32370 |
. . . . . . . . . . . 12
      
               
                   
                   
       
        |
77 | 76 | a1d 26 |
. . . . . . . . . . 11
      
               
                   
          
         
       
         |
78 | 75, 77 | cnfn2dd 32322 |
. . . . . . . . . 10
      
               
                   
          
     
   
    |
79 | 65, 78 | cnfn2dd 32322 |
. . . . . . . . 9
      
               
                   
          
       
    |
80 | 40 | a1d 26 |
. . . . . . . . . . . . . . . 16
      
               
                   
          
           
                 
     
               |
81 | 70, 80 | cnf2dd 32320 |
. . . . . . . . . . . . . . 15
      
               
                   
          
             
          |
82 | 50 | a1d 26 |
. . . . . . . . . . . . . . 15
      
               
                   
          
                  
           |
83 | 81, 82 | cnf2dd 32320 |
. . . . . . . . . . . . . 14
      
               
                   
          
       |
84 | 83, 53 | syld 45 |
. . . . . . . . . . . . 13
      
               
                   
          
     |
85 | | tsbi4 32371 |
. . . . . . . . . . . . . 14
      
               
                   
            
     |
86 | 85 | a1d 26 |
. . . . . . . . . . . . 13
      
               
                   
          
   
     |
87 | 84, 86 | cnfn2dd 32322 |
. . . . . . . . . . . 12
      
               
                   
          
     |
88 | 65, 87 | cnfn1dd 32321 |
. . . . . . . . . . 11
      
               
                   
          
   |
89 | 88 | a1dd 47 |
. . . . . . . . . 10
      
               
                   
          
  
    |
90 | | tsbi1 32368 |
. . . . . . . . . . . 12
      
               
                   
                
   
             
         |
91 | 90 | a1d 26 |
. . . . . . . . . . 11
      
               
                   
          
 
       
           
             |
92 | 91 | or32dd 32323 |
. . . . . . . . . 10
      
               
                   
          
 
       
         
               |
93 | 89, 92 | cnfn2dd 32322 |
. . . . . . . . 9
      
               
                   
          

                 
          |
94 | 79, 93 | cnfn1dd 32321 |
. . . . . . . 8
      
               
                   
          
     
            |
95 | 43 | a1d 26 |
. . . . . . . . 9
      
               
                   
          
         
                   
           |
96 | 81, 95 | cnf2dd 32320 |
. . . . . . . 8
      
               
                   
          
        
         |
97 | 94, 96 | contrd 32326 |
. . . . . . 7
      
               
                   
           |
98 | 97 | efald2 32304 |
. . . . . 6
      
           
                   
              |
99 | 19, 98 | ax-mp 5 |
. . . . 5
            
                   
          |
100 | 3, 99 | ax-mp 5 |
. . . 4
                
         |
101 | 6 | a1i 11 |
. . . . . . 7
     |
102 | | id 22 |
. . . . . . . . . . . 12
    

            
     
     
      
                 
     
     
         |
103 | | tsim2 32366 |
. . . . . . . . . . . . . . 15
    

            
     
     
      
              
     |
104 | 103 | ord 379 |
. . . . . . . . . . . . . 14
    

            
     
     
      
              
     |
105 | 104 | a1dd 47 |
. . . . . . . . . . . . 13
    

            
     
     
      
            
     
           
      |
106 | 105 | a1dd 47 |
. . . . . . . . . . . 12
    

            
     
     
      
                    
     
     
          |
107 | 102, 106 | mt3d 129 |
. . . . . . . . . . 11
    

            
     
     
      
    |
108 | 107 | a1d 26 |
. . . . . . . . . 10
    

            
     
     
      

     |
109 | | simplim 155 |
. . . . . . . . . 10
    

            
     
     
      
      |
110 | 108, 109 | syld 45 |
. . . . . . . . 9
    

            
     
     
      
    |
111 | | tsim2 32366 |
. . . . . . . . . . . . . 14
    

            
     
     
      
            
               
     
     
         |
112 | 111 | ord 379 |
. . . . . . . . . . . . 13
    

            
     
     
      
 
       
     
            
     
     
         |
113 | 112 | a1dd 47 |
. . . . . . . . . . . 12
    

            
     
     
      
 
       
     
        
     
     
           
       |
114 | 102, 113 | mt3d 129 |
. . . . . . . . . . 11
    

            
     
     
      
           
     |
115 | 108, 114 | syld 45 |
. . . . . . . . . 10
    

            
     
     
      
      
        |
116 | | id 22 |
. . . . . . . . . . . . . . . . . 18
           

          
     |
117 | 116 | notornotel2 32325 |
. . . . . . . . . . . . . . . . 17
           

   |
118 | 117 | a1i 11 |
. . . . . . . . . . . . . . . 16
    

            
     
     
      
 
     
         |
119 | 116 | notornotel1 32324 |
. . . . . . . . . . . . . . . . . 18
           

         
    |
120 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    

            
     
     
      
 
     
           
        |
121 | | tsbi3 32370 |
. . . . . . . . . . . . . . . . . 18
    

            
     
     
      
         
 
        
     |
122 | 121 | a1d 26 |
. . . . . . . . . . . . . . . . 17
    

            
     
     
      
 
     
                
      
         |
123 | 120, 122 | cnfn2dd 32322 |
. . . . . . . . . . . . . . . 16
    

            
     
     
      
 
     
           
   
    |
124 | 118, 123 | cnfn2dd 32322 |
. . . . . . . . . . . . . . 15
    

            
     
     
      
 
     
             
    |
125 | | a1tru 1459 |
. . . . . . . . . . . . . . . . 17
    

            
     
     
      
 |
126 | 125 | a1d 26 |
. . . . . . . . . . . . . . . 16
    

            
     
     
      
 
     
        |
127 | | tsbi1 32368 |
. . . . . . . . . . . . . . . . . 18
    

            
     
     
      
 
       
         
    |
128 | 127 | a1d 26 |
. . . . . . . . . . . . . . . . 17
    

            
     
     
      
 
     
               
         
     |
129 | 128 | or32dd 32323 |
. . . . . . . . . . . . . . . 16
    

            
     
     
      
 
     
               
         
     |
130 | 126, 129 | cnfn2dd 32322 |
. . . . . . . . . . . . . . 15
    

            
     
     
      
 
     
           
   
     
        |
131 | 124, 130 | cnfn1dd 32321 |
. . . . . . . . . . . . . 14
    

            
     
     
      
 
     
           
       |
132 | 131 | a1dd 47 |
. . . . . . . . . . . . 13
    

            
     
     
      
 
     
        
     
        |
133 | 132 | a1dd 47 |
. . . . . . . . . . . 12
    

            
     
     
      
 
     
                  
     
     
         |
134 | | ax-1 6 |
. . . . . . . . . . . . 13
    

            
     
     
      
 
     
     
        
     
     
           
       |
135 | | tsim3 32367 |
. . . . . . . . . . . . . 14
    

            
     
     
      
    
     
     
           
      

            
     
     
          |
136 | 135 | a1d 26 |
. . . . . . . . . . . . 13
    

            
     
     
      
 
     
                
     
           
      

            
     
     
           |
137 | 134, 136 | cnf2dd 32320 |
. . . . . . . . . . . 12
    

            
     
     
      
 
     
     
            
     
     
         |
138 | 133, 137 | contrd 32326 |
. . . . . . . . . . 11
    

            
     
     
      
         
     |
139 | 138 | a1d 26 |
. . . . . . . . . 10
    

            
     
     
      
          
      |
140 | 115, 139 | cnfn1dd 32321 |
. . . . . . . . 9
    

            
     
     
      

   |
141 | 110, 140 | contrd 32326 |
. . . . . . . 8
    

            
     
     
      
 |
142 | 141 | efald2 32304 |
. . . . . . 7
        
     
     
           
     |
143 | 101, 142 | ax-mp 5 |
. . . . . 6
            
     
     
       |
144 | 10, 143 | ax-mp 5 |
. . . . 5
           
   |
145 | | ax-1 6 |
. . . . . . . . . 10
    
     
            
     
    ![]() |