Step | Hyp | Ref
| Expression |
1 | | opelxpi 4659 |
. . . 4
 
        |
2 | | enq0ex 7438 |
. . . . 5
~Q0  |
3 | 2 | ecelqsi 6589 |
. . . 4
  
       
~Q0    
~Q0   |
4 | 1, 3 | syl 14 |
. . 3
 
      ~Q0    
~Q0   |
5 | | opelxpi 4659 |
. . . 4
 
        |
6 | 2 | ecelqsi 6589 |
. . . 4
  
       
~Q0    
~Q0   |
7 | 5, 6 | syl 14 |
. . 3
 
      ~Q0    
~Q0   |
8 | 4, 7 | anim12i 338 |
. 2
      
      ~Q0    
~Q0     
~Q0    
~Q0    |
9 | | eqid 2177 |
. . . 4
    
~Q0     
~Q0 |
10 | | eqid 2177 |
. . . 4
    
~Q0     
~Q0 |
11 | 9, 10 | pm3.2i 272 |
. . 3
      ~Q0      ~Q0      ~Q0      ~Q0  |
12 | | eqid 2177 |
. . 3
            
~Q0             
~Q0 |
13 | | opeq12 3781 |
. . . . . . . . 9
 
         |
14 | 13 | eceq1d 6571 |
. . . . . . . 8
 
      ~Q0      ~Q0  |
15 | 14 | eqeq2d 2189 |
. . . . . . 7
 
      
~Q0     
~Q0      ~Q0      ~Q0   |
16 | 15 | anbi1d 465 |
. . . . . 6
 
       
~Q0     
~Q0     
~Q0     
~Q0      
~Q0     
~Q0     
~Q0     
~Q0    |
17 | | simpl 109 |
. . . . . . . . . . 11
 
   |
18 | 17 | oveq1d 5890 |
. . . . . . . . . 10
 
       |
19 | | simpr 110 |
. . . . . . . . . . 11
 
   |
20 | 19 | oveq1d 5890 |
. . . . . . . . . 10
 
       |
21 | 18, 20 | oveq12d 5893 |
. . . . . . . . 9
 
               |
22 | 19 | oveq1d 5890 |
. . . . . . . . 9
 
       |
23 | 21, 22 | opeq12d 3787 |
. . . . . . . 8
 
                         |
24 | 23 | eceq1d 6571 |
. . . . . . 7
 
              ~Q0              ~Q0  |
25 | 24 | eqeq2d 2189 |
. . . . . 6
 
              
~Q0             
~Q0              ~Q0              ~Q0   |
26 | 16, 25 | anbi12d 473 |
. . . . 5
 
         ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0        ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0    |
27 | 26 | spc2egv 2828 |
. . . 4
 
         ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0
           ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0    |
28 | | opeq12 3781 |
. . . . . . . . . 10
 
         |
29 | 28 | eceq1d 6571 |
. . . . . . . . 9
 
      ~Q0      ~Q0  |
30 | 29 | eqeq2d 2189 |
. . . . . . . 8
 
      
~Q0     
~Q0      ~Q0      ~Q0   |
31 | 30 | anbi2d 464 |
. . . . . . 7
 
       
~Q0     
~Q0     
~Q0     
~Q0      
~Q0     
~Q0     
~Q0     
~Q0    |
32 | | simpr 110 |
. . . . . . . . . . . 12
 
   |
33 | 32 | oveq2d 5891 |
. . . . . . . . . . 11
 
       |
34 | | simpl 109 |
. . . . . . . . . . . 12
 
   |
35 | 34 | oveq2d 5891 |
. . . . . . . . . . 11
 
       |
36 | 33, 35 | oveq12d 5893 |
. . . . . . . . . 10
 
               |
37 | 32 | oveq2d 5891 |
. . . . . . . . . 10
 
       |
38 | 36, 37 | opeq12d 3787 |
. . . . . . . . 9
 
                         |
39 | 38 | eceq1d 6571 |
. . . . . . . 8
 
              ~Q0              ~Q0  |
40 | 39 | eqeq2d 2189 |
. . . . . . 7
 
              
~Q0             
~Q0              ~Q0              ~Q0   |
41 | 31, 40 | anbi12d 473 |
. . . . . 6
 
         ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0        ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0    |
42 | 41 | spc2egv 2828 |
. . . . 5
 
         ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0
           ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0    |
43 | 42 | 2eximdv 1882 |
. . . 4
 
             ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0
               ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0    |
44 | 27, 43 | sylan9 409 |
. . 3
      
       
~Q0     
~Q0     
~Q0     
~Q0             
~Q0             
~Q0
               ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0    |
45 | 11, 12, 44 | mp2ani 432 |
. 2
      
               ~Q0      ~Q0      ~Q0      ~Q0             
~Q0             
~Q0   |
46 | | ecexg 6539 |
. . . 4
~Q0
             ~Q0   |
47 | 2, 46 | ax-mp 5 |
. . 3
            
~Q0  |
48 | | simp1 997 |
. . . . . . . 8
      
~Q0      ~Q0
            
~Q0
     ~Q0  |
49 | 48 | eqeq1d 2186 |
. . . . . . 7
      
~Q0      ~Q0
            
~Q0
      ~Q0      ~Q0      ~Q0   |
50 | | simp2 998 |
. . . . . . . 8
      
~Q0      ~Q0
            
~Q0
     ~Q0  |
51 | 50 | eqeq1d 2186 |
. . . . . . 7
      
~Q0      ~Q0
            
~Q0
      ~Q0      ~Q0      ~Q0   |
52 | 49, 51 | anbi12d 473 |
. . . . . 6
      
~Q0      ~Q0
            
~Q0
      
~Q0      ~Q0      
~Q0     
~Q0     
~Q0     
~Q0    |
53 | | simp3 999 |
. . . . . . 7
      
~Q0      ~Q0
            
~Q0
             ~Q0  |
54 | 53 | eqeq1d 2186 |
. . . . . 6
      
~Q0      ~Q0
            
~Q0
              ~Q0             
~Q0             
~Q0   |
55 | 52, 54 | anbi12d 473 |
. . . . 5
      
~Q0      ~Q0
            
~Q0
        ~Q0     
~Q0              ~Q0       
~Q0     
~Q0     
~Q0     
~Q0             
~Q0             
~Q0    |
56 | 55 | 4exbidv 1870 |
. . . 4
      
~Q0      ~Q0
            
~Q0
               
~Q0      ~Q0              ~Q0               
~Q0     
~Q0     
~Q0     
~Q0             
~Q0             
~Q0    |
57 | | addnq0mo 7446 |
. . . 4
      ~Q0     ~Q0                   ~Q0     
~Q0              ~Q0   |
58 | | dfplq0qs 7429 |
. . . 4
+Q0       
      ~Q0     ~Q0                
~Q0      ~Q0              ~Q0    |
59 | 56, 57, 58 | ovig 5996 |
. . 3
       ~Q0    
~Q0     
~Q0    
~Q0             
~Q0                 
~Q0     
~Q0     
~Q0     
~Q0             
~Q0             
~Q0
      ~Q0
+Q0      ~Q0
            
~Q0   |
60 | 47, 59 | mp3an3 1326 |
. 2
       ~Q0    
~Q0     
~Q0    
~Q0                 
~Q0     
~Q0     
~Q0     
~Q0             
~Q0             
~Q0
      ~Q0
+Q0      ~Q0
            
~Q0   |
61 | 8, 45, 60 | sylc 62 |
1
      
      ~Q0
+Q0      ~Q0
            
~Q0  |