Step | Hyp | Ref
| Expression |
1 | | elxp 4305 |
. . . . . . . 8
  
        
    |
2 | | elxp 4305 |
. . . . . . . 8
  
        
    |
3 | | elxp 4305 |
. . . . . . . 8
  
        
    |
4 | | 3an6 1216 |
. . . . . . . . . . . . . . . . 17
      
      
 

  

  
               
 
     |
5 | | poirr 4035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
     |
6 | 5 | ex 108 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
7 | | poirr 4035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
     |
8 | 7 | intnand 839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
       |
9 | 8 | ex 108 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
10 | 6, 9 | im2anan9 530 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
               |
11 | | ioran 668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
12 | 10, 11 | syl6ibr 151 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
               |
13 | 12 | imp 115 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
              |
14 | 13 | intnand 839 |
. . . . . . . . . . . . . . . . . . . . . 22
  
        
             |
15 | 14 | 3ad2antr1 1068 |
. . . . . . . . . . . . . . . . . . . . 21
  
    
 
       
             |
16 | | an4 520 |
. . . . . . . . . . . . . . . . . . . . . 22
      
             
                 
     
                          |
17 | | 3an6 1216 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
   
     
    |
18 | | potr 4036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  
 
            |
19 | 18 | 3impia 1100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  
            |
20 | 19 | orcd 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  
                  |
21 | 20 | 3expia 1105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  
 
                  |
22 | 21 | expdimp 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
                 |
23 | | breq2 3759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
         |
24 | 23 | biimpa 280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
         |
25 | 24 | orcd 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
               |
26 | 25 | expcom 109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
               |
27 | 26 | adantrd 264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
              |
28 | 27 | adantl 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
                   |
29 | 22, 28 | jaod 636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
                       |
30 | 29 | ex 108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
 
                        |
31 | | potr 4036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  
 
            |
32 | 31 | expdimp 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
 
           |
33 | 32 | anim2d 320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
 
               |
34 | 33 | orim2d 701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
 
                       |
35 | | breq1 3758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
         |
36 | | equequ1 1595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
37 | 36 | anbi1d 438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  
          |
38 | 35, 37 | orbi12d 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                     |
39 | 38 | imbi2d 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                         |
40 | 34, 39 | syl5ibr 145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
 
                        |
41 | 40 | expd 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  

 
                         |
42 | 41 | com12 27 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
 
                          |
43 | 42 | impd 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
 
 
                        |
44 | 30, 43 | jaao 638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
 


                                 |
45 | 44 | impd 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 


                                 |
46 | 45 | an4s 522 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
    
  
                              |
47 | 17, 46 | sylan2b 271 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
    
 
                                 |
48 | | an4 520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
     
 
    |
49 | 48 | biimpi 113 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
     
      |
50 | 49 | 3adant2 922 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
   
     
    |
51 | 50 | adantl 262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
    
 
    
      |
52 | 47, 51 | jctild 299 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    
 
                          
              |
53 | 52 | adantld 263 |
. . . . . . . . . . . . . . . . . . . . . 22
  
    
 
         
     
  
                     
                |
54 | 16, 53 | syl5bi 141 |
. . . . . . . . . . . . . . . . . . . . 21
  
    
 
         
             
                
                |
55 | 15, 54 | jca 290 |
. . . . . . . . . . . . . . . . . . . 20
  
    
 
        
                 
             
                
                 |
56 | | breq12 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
              |
57 | 56 | anidms 377 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                  |
58 | 57 | notbid 591 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  |
59 | 58 | 3ad2ant1 924 |
. . . . . . . . . . . . . . . . . . . . . 22
                          |
60 | | breq12 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
              |
61 | 60 | 3adant3 923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                          |
62 | | breq12 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
              |
63 | 62 | 3adant1 921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                          |
64 | 61, 63 | anbi12d 442 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                        |
65 | | breq12 3760 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
              |
66 | 65 | 3adant2 922 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          |
67 | 64, 66 | imbi12d 223 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                      |
68 | 59, 67 | anbi12d 442 |
. . . . . . . . . . . . . . . . . . . . 21
                                                      
             |
69 | | poxp.1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
    
                                   |
70 | 69 | xporderlem 5793 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
               |
71 | 70 | notbii 593 |
. . . . . . . . . . . . . . . . . . . . . 22
           
 
 
           |
72 | 69 | xporderlem 5793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
               |
73 | 69 | xporderlem 5793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
               |
74 | 72, 73 | anbi12i 433 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  
   
                 
              |
75 | 69 | xporderlem 5793 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
               |
76 | 74, 75 | imbi12i 228 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
             
 
 
           
                
                |
77 | 71, 76 | anbi12i 433 |
. . . . . . . . . . . . . . . . . . . . 21
                                            
                 
             
                
                 |
78 | 68, 77 | syl6bb 185 |
. . . . . . . . . . . . . . . . . . . 20
                              
                 
                 
              
                  |
79 | 55, 78 | syl5ibr 145 |
. . . . . . . . . . . . . . . . . . 19
                 
   
  
                 |
80 | 79 | expcomd 1327 |
. . . . . . . . . . . . . . . . . 18
                
 
 
 
                   |
81 | 80 | imp 115 |
. . . . . . . . . . . . . . . . 17
                
 
    
                  |
82 | 4, 81 | sylbi 114 |
. . . . . . . . . . . . . . . 16
      
      
 

  

  
 
                  |
83 | 82 | 3exp 1102 |
. . . . . . . . . . . . . . 15
     
               
                        |
84 | 83 | com3l 75 |
. . . . . . . . . . . . . 14
     
               
                        |
85 | 84 | exlimivv 1773 |
. . . . . . . . . . . . 13
                 
           
                    |
86 | 85 | com3l 75 |
. . . . . . . . . . . 12
    

               
   
                        |
87 | 86 | exlimivv 1773 |
. . . . . . . . . . 11
                 
           
 
 
                    |
88 | 87 | com3l 75 |
. . . . . . . . . 10
     
           
 
        

                        |
89 | 88 | exlimivv 1773 |
. . . . . . . . 9
                 
   
           
 
 
                    |
90 | 89 | 3imp 1097 |
. . . . . . . 8
          
          
 
        
    
                  |
91 | 1, 2, 3, 90 | syl3anb 1177 |
. . . . . . 7
   
    
 
                  |
92 | 91 | 3expia 1105 |
. . . . . 6
   
   
   
                   |
93 | 92 | com3r 73 |
. . . . 5
 
          
                  |
94 | 93 | imp 115 |
. . . 4
  
        
                   |
95 | 94 | ralrimiv 2385 |
. . 3
  
        
                   |
96 | 95 | ralrimivva 2395 |
. 2
 
     
   
                   |
97 | | df-po 4024 |
. 2
  
        
                   |
98 | 96, 97 | sylibr 137 |
1
 
     |