Step | Hyp | Ref
| Expression |
1 | | enq0er 7433 |
. . . . . . . . . . . . . 14
~Q0    |
2 | 1 | a1i 9 |
. . . . . . . . . . . . 13
       ~Q0     ~Q0          ~Q0
     ~Q0          ~Q0       
~Q0      ~Q0
         ~Q0  
~Q0     |
3 | | nnnq0lem1 7444 |
. . . . . . . . . . . . . 14
       ~Q0     ~Q0          ~Q0
     ~Q0          ~Q0       
~Q0      ~Q0
         ~Q0        
 
 
          
       |
4 | | mulcmpblnq0 7442 |
. . . . . . . . . . . . . . 15
   


 
 
               
       ~Q0           |
5 | 4 | imp 124 |
. . . . . . . . . . . . . 14
      
 
 
          
    
       ~Q0          |
6 | 3, 5 | syl 14 |
. . . . . . . . . . . . 13
       ~Q0     ~Q0          ~Q0
     ~Q0          ~Q0       
~Q0      ~Q0
         ~Q0         
~Q0          |
7 | 2, 6 | erthi 6580 |
. . . . . . . . . . . 12
       ~Q0     ~Q0          ~Q0
     ~Q0          ~Q0       
~Q0      ~Q0
         ~Q0           
~Q0         
~Q0  |
8 | | simprlr 538 |
. . . . . . . . . . . 12
       ~Q0     ~Q0          ~Q0
     ~Q0          ~Q0       
~Q0      ~Q0
         ~Q0            ~Q0  |
9 | | simprrr 540 |
. . . . . . . . . . . 12
       ~Q0     ~Q0          ~Q0
     ~Q0          ~Q0       
~Q0      ~Q0
         ~Q0            ~Q0  |
10 | 7, 8, 9 | 3eqtr4d 2220 |
. . . . . . . . . . 11
       ~Q0     ~Q0          ~Q0
     ~Q0          ~Q0       
~Q0      ~Q0
         ~Q0     |
11 | 10 | expr 375 |
. . . . . . . . . 10
       ~Q0     ~Q0         ~Q0     
~Q0          ~Q0          ~Q0
     ~Q0
         ~Q0    |
12 | 11 | exlimdvv 1897 |
. . . . . . . . 9
       ~Q0     ~Q0         ~Q0     
~Q0          ~Q0              ~Q0     
~Q0          ~Q0    |
13 | 12 | exlimdvv 1897 |
. . . . . . . 8
       ~Q0     ~Q0         ~Q0     
~Q0          ~Q0                  ~Q0     
~Q0          ~Q0    |
14 | 13 | ex 115 |
. . . . . . 7
      ~Q0     ~Q0          ~Q0
     ~Q0          ~Q0                
~Q0      ~Q0
         ~Q0     |
15 | 14 | exlimdvv 1897 |
. . . . . 6
      ~Q0     ~Q0              ~Q0     
~Q0          ~Q0                
~Q0      ~Q0
         ~Q0     |
16 | 15 | exlimdvv 1897 |
. . . . 5
      ~Q0     ~Q0                  ~Q0     
~Q0          ~Q0                
~Q0      ~Q0
         ~Q0     |
17 | 16 | impd 254 |
. . . 4
      ~Q0     ~Q0                   ~Q0
     ~Q0          ~Q0               
~Q0      ~Q0
         ~Q0 
   |
18 | 17 | alrimivv 1875 |
. . 3
      ~Q0     ~Q0                       ~Q0     
~Q0          ~Q0               
~Q0      ~Q0
         ~Q0 
   |
19 | | opeq12 3780 |
. . . . . . . . . . 11
 
         |
20 | 19 | eceq1d 6570 |
. . . . . . . . . 10
 
      ~Q0      ~Q0  |
21 | 20 | eqeq2d 2189 |
. . . . . . . . 9
 
       ~Q0      ~Q0   |
22 | 21 | anbi1d 465 |
. . . . . . . 8
 
        ~Q0
     ~Q0       ~Q0     
~Q0    |
23 | | simpl 109 |
. . . . . . . . . . . 12
 
   |
24 | 23 | oveq1d 5889 |
. . . . . . . . . . 11
 
       |
25 | | simpr 110 |
. . . . . . . . . . . 12
 
   |
26 | 25 | oveq1d 5889 |
. . . . . . . . . . 11
 
       |
27 | 24, 26 | opeq12d 3786 |
. . . . . . . . . 10
 
                 |
28 | 27 | eceq1d 6570 |
. . . . . . . . 9
 
          ~Q0          ~Q0  |
29 | 28 | eqeq2d 2189 |
. . . . . . . 8
 
           ~Q0          ~Q0   |
30 | 22, 29 | anbi12d 473 |
. . . . . . 7
 
        
~Q0      ~Q0          ~Q0        ~Q0
     ~Q0          ~Q0    |
31 | | opeq12 3780 |
. . . . . . . . . . 11
 
         |
32 | 31 | eceq1d 6570 |
. . . . . . . . . 10
 
      ~Q0      ~Q0  |
33 | 32 | eqeq2d 2189 |
. . . . . . . . 9
 
       ~Q0      ~Q0   |
34 | 33 | anbi2d 464 |
. . . . . . . 8
 
        ~Q0
     ~Q0       ~Q0     
~Q0    |
35 | | simpl 109 |
. . . . . . . . . . . 12
 
   |
36 | 35 | oveq2d 5890 |
. . . . . . . . . . 11
 
       |
37 | | simpr 110 |
. . . . . . . . . . . 12
 
   |
38 | 37 | oveq2d 5890 |
. . . . . . . . . . 11
 
       |
39 | 36, 38 | opeq12d 3786 |
. . . . . . . . . 10
 
                 |
40 | 39 | eceq1d 6570 |
. . . . . . . . 9
 
          ~Q0          ~Q0  |
41 | 40 | eqeq2d 2189 |
. . . . . . . 8
 
           ~Q0          ~Q0   |
42 | 34, 41 | anbi12d 473 |
. . . . . . 7
 
        
~Q0      ~Q0          ~Q0        ~Q0
     ~Q0
         ~Q0    |
43 | 30, 42 | cbvex4v 1930 |
. . . . . 6
                ~Q0     
~Q0          ~Q0                ~Q0     
~Q0          ~Q0   |
44 | 43 | anbi2i 457 |
. . . . 5
                 ~Q0     
~Q0          ~Q0                ~Q0
     ~Q0          ~Q0                 
~Q0      ~Q0          ~Q0               
~Q0      ~Q0
         ~Q0    |
45 | 44 | imbi1i 238 |
. . . 4
                  ~Q0
     ~Q0          ~Q0                ~Q0
     ~Q0          ~Q0 

                 ~Q0     
~Q0          ~Q0               
~Q0      ~Q0
         ~Q0 
   |
46 | 45 | 2albii 1471 |
. . 3
                      ~Q0     
~Q0          ~Q0                ~Q0
     ~Q0          ~Q0 

                     ~Q0     
~Q0          ~Q0               
~Q0      ~Q0
         ~Q0 
   |
47 | 18, 46 | sylibr 134 |
. 2
      ~Q0     ~Q0                       ~Q0     
~Q0          ~Q0                ~Q0
     ~Q0          ~Q0 
   |
48 | | eqeq1 2184 |
. . . . 5
          
~Q0         
~Q0   |
49 | 48 | anbi2d 464 |
. . . 4
         ~Q0
     ~Q0          ~Q0        ~Q0
     ~Q0          ~Q0    |
50 | 49 | 4exbidv 1870 |
. . 3
                 ~Q0     
~Q0          ~Q0                ~Q0     
~Q0          ~Q0    |
51 | 50 | mo4 2087 |
. 2
                  ~Q0
     ~Q0          ~Q0                      ~Q0
     ~Q0          ~Q0                ~Q0
     ~Q0          ~Q0 
   |
52 | 47, 51 | sylibr 134 |
1
      ~Q0     ~Q0                   ~Q0     
~Q0          ~Q0   |