Step | Hyp | Ref
| Expression |
1 | | elxp 4640 |
. . . . . . . 8
  
        
    |
2 | | elxp 4640 |
. . . . . . . 8
  
        
    |
3 | | elxp 4640 |
. . . . . . . 8
  
        
    |
4 | | 3an6 1322 |
. . . . . . . . . . . . . . . . 17
      
 
           
  
               
 
     |
5 | | poirr 4304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
     |
6 | 5 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
7 | | poirr 4304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
     |
8 | 7 | intnand 931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
       |
9 | 8 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
10 | 6, 9 | im2anan9 598 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
               |
11 | | ioran 752 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
          |
12 | 10, 11 | syl6ibr 162 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
               |
13 | 12 | imp 124 |
. . . . . . . . . . . . . . . . . . . . . . 23
  


            |
14 | 13 | intnand 931 |
. . . . . . . . . . . . . . . . . . . . . 22
  


      
 
           |
15 | 14 | 3ad2antr1 1162 |
. . . . . . . . . . . . . . . . . . . . 21
  

 
 


  
  


             |
16 | | an4 586 |
. . . . . . . . . . . . . . . . . . . . . 22
      
 
           


               


     
                        |
17 | | 3an6 1322 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  


 
   
 
    |
18 | | potr 4305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  
        
     |
19 | 18 | 3impia 1200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  

           |
20 | 19 | orcd 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  

                 |
21 | 20 | 3expia 1205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  
        
           |
22 | 21 | expdimp 259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
                   |
23 | | breq2 4004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   
     |
24 | 23 | biimpa 296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
         |
25 | 24 | orcd 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
               |
26 | 25 | expcom 116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
               |
27 | 26 | adantrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
           |
28 | 27 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
                     |
29 | 22, 28 | jaod 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
                         |
30 | 29 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
                          |
31 | | potr 4305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  
        
     |
32 | 31 | expdimp 259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
             |
33 | 32 | anim2d 337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
                 |
34 | 33 | orim2d 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
                         |
35 | | breq1 4003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
     |
36 | | equequ1 1712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
   |
37 | 36 | anbi1d 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             |
38 | 35, 37 | orbi12d 793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         
           |
39 | 38 | imbi2d 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                         |
40 | 34, 39 | syl5ibr 156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                               |
41 | 40 | expd 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
                           |
42 | 41 | com12 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  
                            |
43 | 42 | impd 254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
      
                     |
44 | 30, 43 | jaao 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
  

                                 |
45 | 44 | impd 254 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
  

                     
           |
46 | 45 | an4s 588 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  

 
 
                     
           |
47 | 17, 46 | sylan2b 287 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

 
 


                                 |
48 | | an4 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  


 
 
 
    |
49 | 48 | biimpi 120 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  


     
    |
50 | 49 | 3adant2 1016 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  


 
 
 
 
    |
51 | 50 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

 
 


      
    |
52 | 47, 51 | jctild 316 |
. . . . . . . . . . . . . . . . . . . . . . 23
  

 
 


                          
 
            |
53 | 52 | adantld 278 |
. . . . . . . . . . . . . . . . . . . . . 22
  

 
 


         
 
 
 
                          
 
            |
54 | 16, 53 | biimtrid 152 |
. . . . . . . . . . . . . . . . . . . . 21
  

 
 


         
 
           


           
  


              |
55 | 15, 54 | jca 306 |
. . . . . . . . . . . . . . . . . . . 20
  

 
 


        
 
               
 
           


           
  


               |
56 | | breq12 4005 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
  
           |
57 | 56 | anidms 397 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                  |
58 | 57 | notbid 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
           |
59 | 58 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . . 22
              
           |
60 | | breq12 4005 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
  
           |
61 | 60 | 3adant3 1017 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                          |
62 | | breq12 4005 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
  
           |
63 | 62 | 3adant1 1015 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                          |
64 | 61, 63 | anbi12d 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  
                     |
65 | | breq12 4005 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
  
           |
66 | 65 | 3adant2 1016 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          |
67 | 64, 66 | imbi12d 234 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                      |
68 | 59, 67 | anbi12d 473 |
. . . . . . . . . . . . . . . . . . . . 21
                      
   
                           
             |
69 | | poxp.1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
   
                                      |
70 | 69 | xporderlem 6226 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
 
           |
71 | 70 | notbii 668 |
. . . . . . . . . . . . . . . . . . . . . 22
           
 
             |
72 | 69 | xporderlem 6226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
 
           |
73 | 69 | xporderlem 6226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
 
           |
74 | 72, 73 | anbi12i 460 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  
   


             
 
              |
75 | 69 | xporderlem 6226 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
 
           |
76 | 74, 75 | imbi12i 239 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
             
 
               
 
              
 
            |
77 | 71, 76 | anbi12i 460 |
. . . . . . . . . . . . . . . . . . . . 21
                            
               
 
               
 
           


           
  


               |
78 | 68, 77 | bitrdi 196 |
. . . . . . . . . . . . . . . . . . . 20
                      
   
     
 
               
 
           


           
  


                |
79 | 55, 78 | syl5ibr 156 |
. . . . . . . . . . . . . . . . . . 19
                 


 
                    |
80 | 79 | expcomd 1441 |
. . . . . . . . . . . . . . . . . 18
                
 
   

         
        |
81 | 80 | imp 124 |
. . . . . . . . . . . . . . . . 17
                
 
     
         
       |
82 | 4, 81 | sylbi 121 |
. . . . . . . . . . . . . . . 16
      
 
           
    

         
       |
83 | 82 | 3exp 1202 |
. . . . . . . . . . . . . . 15
     
 
     
 
     
 
 
                    |
84 | 83 | com3l 81 |
. . . . . . . . . . . . . 14
     
 
     
 
     
 
 
                    |
85 | 84 | exlimivv 1896 |
. . . . . . . . . . . . 13
         
 
     
 
     
 
 
                    |
86 | 85 | com3l 81 |
. . . . . . . . . . . 12
     
 
     
 
              
         
         |
87 | 86 | exlimivv 1896 |
. . . . . . . . . . 11
         
 
     
 
              
         
         |
88 | 87 | com3l 81 |
. . . . . . . . . 10
     
 
                     
   

         
         |
89 | 88 | exlimivv 1896 |
. . . . . . . . 9
         
 
                     
   

         
         |
90 | 89 | 3imp 1193 |
. . . . . . . 8
          
 
        
                                  |
91 | 1, 2, 3, 90 | syl3anb 1281 |
. . . . . . 7
   
      

         
       |
92 | 91 | 3expia 1205 |
. . . . . 6
   
                           |
93 | 92 | com3r 79 |
. . . . 5
 
    

                       |
94 | 93 | imp 124 |
. . . 4
  

  

               
       |
95 | 94 | ralrimiv 2549 |
. . 3
  

  

   
                   |
96 | 95 | ralrimivva 2559 |
. 2
 
                             |
97 | | df-po 4293 |
. 2
  
                     
      |
98 | 96, 97 | sylibr 134 |
1
 
     |