Proof of Theorem nnnq0lem1
Step | Hyp | Ref
| Expression |
1 | | enq0er 7433 |
. . . . . 6
~Q0    |
2 | | erdm 6544 |
. . . . . 6
~Q0
  ~Q0     |
3 | 1, 2 | ax-mp 5 |
. . . . 5
~Q0    |
4 | | simpll 527 |
. . . . . 6
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0  
    ~Q0   |
5 | | simplll 533 |
. . . . . . . 8
         ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       ~Q0  |
6 | 5 | eleq1d 2246 |
. . . . . . 7
         ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0  
    ~Q0
    
~Q0    
~Q0    |
7 | 6 | adantl 277 |
. . . . . 6
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0        ~Q0      ~Q0    
~Q0    |
8 | 4, 7 | mpbid 147 |
. . . . 5
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0        ~Q0    
~Q0   |
9 | | ecelqsdm 6604 |
. . . . 5
  ~Q0  
    
~Q0    
~Q0         |
10 | 3, 8, 9 | sylancr 414 |
. . . 4
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0          |
11 | | opelxp 4656 |
. . . 4
          |
12 | 10, 11 | sylib 122 |
. . 3
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       |
13 | | simprll 537 |
. . . . . . . 8
         ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       ~Q0  |
14 | 13 | eleq1d 2246 |
. . . . . . 7
         ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0  
    ~Q0
    
~Q0    
~Q0    |
15 | 14 | adantl 277 |
. . . . . 6
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0        ~Q0      ~Q0    
~Q0    |
16 | 4, 15 | mpbid 147 |
. . . . 5
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0        ~Q0    
~Q0   |
17 | | ecelqsdm 6604 |
. . . . 5
  ~Q0  
    
~Q0    
~Q0         |
18 | 3, 16, 17 | sylancr 414 |
. . . 4
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0          |
19 | | opelxp 4656 |
. . . 4
          |
20 | 18, 19 | sylib 122 |
. . 3
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       |
21 | 12, 20 | jca 306 |
. 2
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0    


    |
22 | | simplr 528 |
. . . . . 6
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0  
    ~Q0   |
23 | | simpllr 534 |
. . . . . . . 8
         ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       ~Q0  |
24 | 23 | eleq1d 2246 |
. . . . . . 7
         ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0  
    ~Q0
    
~Q0    
~Q0    |
25 | 24 | adantl 277 |
. . . . . 6
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0        ~Q0      ~Q0    
~Q0    |
26 | 22, 25 | mpbid 147 |
. . . . 5
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0        ~Q0    
~Q0   |
27 | | ecelqsdm 6604 |
. . . . 5
  ~Q0  
    
~Q0    
~Q0         |
28 | 3, 26, 27 | sylancr 414 |
. . . 4
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0          |
29 | | opelxp 4656 |
. . . 4
          |
30 | 28, 29 | sylib 122 |
. . 3
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       |
31 | | simprlr 538 |
. . . . . . . 8
         ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       ~Q0  |
32 | 31 | eleq1d 2246 |
. . . . . . 7
         ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0  
    ~Q0
    
~Q0    
~Q0    |
33 | 32 | adantl 277 |
. . . . . 6
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0        ~Q0      ~Q0    
~Q0    |
34 | 22, 33 | mpbid 147 |
. . . . 5
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0        ~Q0    
~Q0   |
35 | | ecelqsdm 6604 |
. . . . 5
  ~Q0  
    
~Q0    
~Q0    
    |
36 | 3, 34, 35 | sylancr 414 |
. . . 4
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0          |
37 | | opelxp 4656 |
. . . 4
          |
38 | 36, 37 | sylib 122 |
. . 3
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       |
39 | 30, 38 | jca 306 |
. 2
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0    


    |
40 | 5, 13 | eqtr3d 2212 |
. . . . . 6
         ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0      
~Q0     
~Q0  |
41 | 40 | adantl 277 |
. . . . 5
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0        ~Q0      ~Q0  |
42 | 1 | a1i 9 |
. . . . . 6
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0   ~Q0     |
43 | 42, 10 | erth 6578 |
. . . . 5
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       ~Q0   
    
~Q0     
~Q0   |
44 | 41, 43 | mpbird 167 |
. . . 4
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0      ~Q0      |
45 | | enq0breq 7434 |
. . . . 5
      
   
~Q0           |
46 | 12, 20, 45 | syl2anc 411 |
. . . 4
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       ~Q0   
       |
47 | 44, 46 | mpbid 147 |
. . 3
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0         |
48 | 23, 31 | eqtr3d 2212 |
. . . . . 6
         ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0      
~Q0     
~Q0  |
49 | 48 | adantl 277 |
. . . . 5
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0        ~Q0      ~Q0  |
50 | 42, 28 | erth 6578 |
. . . . 5
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       ~Q0   
    
~Q0     
~Q0   |
51 | 49, 50 | mpbird 167 |
. . . 4
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0      ~Q0      |
52 | | enq0breq 7434 |
. . . . 5
      
   
~Q0           |
53 | 30, 38, 52 | syl2anc 411 |
. . . 4
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0       ~Q0   
       |
54 | 51, 53 | mpbid 147 |
. . 3
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0         |
55 | 47, 54 | jca 306 |
. 2
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0               |
56 | 21, 39, 55 | jca31 309 |
1
       ~Q0     ~Q0          ~Q0
     ~Q0  
~Q0       
~Q0      ~Q0
 
~Q0      
   
 
          
       |