Proof of Theorem suppr
| Step | Hyp | Ref
| Expression |
| 1 | | ifcl 3007 |
. . . 4
            |
| 2 | | breq2 3342 |
. . . . . . . . . . . . . 14
         |
| 3 | 2 | notbid 673 |
. . . . . . . . . . . . 13
         |
| 4 | | suppr.1 |
. . . . . . . . . . . . . . 15
 |
| 5 | | sonr 3610 |
. . . . . . . . . . . . . . 15
 

    |
| 6 | 4, 5 | mpan 759 |
. . . . . . . . . . . . . 14

    |
| 7 | 6 | ad2antrr 440 |
. . . . . . . . . . . . 13
           |
| 8 | 3, 7 | syl5cbir 228 |
. . . . . . . . . . . 12
             |
| 9 | | breq2 3342 |
. . . . . . . . . . . . . 14
         |
| 10 | 9 | notbid 673 |
. . . . . . . . . . . . 13
         |
| 11 | | so2nr 3613 |
. . . . . . . . . . . . . . . . 17
             |
| 12 | 4, 11 | mpan 759 |
. . . . . . . . . . . . . . . 16
           |
| 13 | | imnan 261 |
. . . . . . . . . . . . . . . 16
               |
| 14 | 12, 13 | sylibr 217 |
. . . . . . . . . . . . . . 15
           |
| 15 | 14 | ancoms 484 |
. . . . . . . . . . . . . 14
           |
| 16 | 15 | imp 377 |
. . . . . . . . . . . . 13
           |
| 17 | 10, 16 | syl5cbir 228 |
. . . . . . . . . . . 12
             |
| 18 | 8, 17 | jaod 469 |
. . . . . . . . . . 11
               |
| 19 | | iftrue 2989 |
. . . . . . . . . . . . . 14
            |
| 20 | 19 | breq1d 3348 |
. . . . . . . . . . . . 13
                  |
| 21 | 20 | notbid 673 |
. . . . . . . . . . . 12
                  |
| 22 | 21 | adantl 424 |
. . . . . . . . . . 11
                      |
| 23 | 18, 22 | sylibrd 221 |
. . . . . . . . . 10
                      |
| 24 | | breq2 3342 |
. . . . . . . . . . . . . 14
         |
| 25 | 24 | notbid 673 |
. . . . . . . . . . . . 13
         |
| 26 | | simpr 350 |
. . . . . . . . . . . . 13
           |
| 27 | 25, 26 | syl5cbir 228 |
. . . . . . . . . . . 12
             |
| 28 | | breq2 3342 |
. . . . . . . . . . . . . 14
         |
| 29 | 28 | notbid 673 |
. . . . . . . . . . . . 13
         |
| 30 | | sonr 3610 |
. . . . . . . . . . . . . . 15
 

    |
| 31 | 4, 30 | mpan 759 |
. . . . . . . . . . . . . 14

    |
| 32 | 31 | ad2antlr 441 |
. . . . . . . . . . . . 13
           |
| 33 | 29, 32 | syl5cbir 228 |
. . . . . . . . . . . 12
             |
| 34 | 27, 33 | jaod 469 |
. . . . . . . . . . 11
               |
| 35 | | iffalse 2991 |
. . . . . . . . . . . . . 14
            |
| 36 | 35 | breq1d 3348 |
. . . . . . . . . . . . 13
                  |
| 37 | 36 | notbid 673 |
. . . . . . . . . . . 12
                  |
| 38 | 37 | adantl 424 |
. . . . . . . . . . 11
                      |
| 39 | 34, 38 | sylibrd 221 |
. . . . . . . . . 10
                      |
| 40 | 23, 39 | pm2.61dan 535 |
. . . . . . . . 9
                  |
| 41 | | visset 2295 |
. . . . . . . . . 10
 |
| 42 | 41 | elpr 3061 |
. . . . . . . . 9
        |
| 43 | 40, 42 | syl5ib 223 |
. . . . . . . 8
                   |
| 44 | 43 | r19.21aiv 2175 |
. . . . . . 7
      
           |
| 45 | | breq2 3342 |
. . . . . . . . . . . 12
                       |
| 46 | 45 | rcla4ev 2381 |
. . . . . . . . . . 11
           
            
      |
| 47 | | ifpr 3077 |
. . . . . . . . . . 11
               |
| 48 | 46, 47 | sylan 497 |
. . . . . . . . . 10
                       |
| 49 | 48 | ex 402 |
. . . . . . . . 9
               
       |
| 50 | 49 | a1d 15 |
. . . . . . . 8
                         |
| 51 | 50 | r19.21aiv 2175 |
. . . . . . 7
   
            
       |
| 52 | | breq1 3341 |
. . . . . . . . . . 11
                       |
| 53 | 52 | notbid 673 |
. . . . . . . . . 10
                       |
| 54 | 53 | ralbidv 2123 |
. . . . . . . . 9
            
    
             |
| 55 | | breq2 3342 |
. . . . . . . . . . 11
                       |
| 56 | 55 | imbi1d 675 |
. . . . . . . . . 10
            
                            |
| 57 | 56 | ralbidv 2123 |
. . . . . . . . 9
         
   
                             |
| 58 | 54, 57 | anbi12d 690 |
. . . . . . . 8
                                                      
           |
| 59 | 58 | rcla4ev 2381 |
. . . . . . 7
                                  
         
 
                    |
| 60 | 1, 44, 51, 59 | syl12anc 1098 |
. . . . . 6
   
 
                    |
| 61 | 4 | supmo 5666 |
. . . . . 6
       
 

   
          |
| 62 | 60, 61 | jctir 317 |
. . . . 5
        
                      
                    |
| 63 | | reu5 2441 |
. . . . 5
      
 

   
              
 

   
              
                    |
| 64 | 62, 63 | sylibr 217 |
. . . 4
                          |
| 65 | 58 | reuuni2 3811 |
. . . 4
                                    
         
                    
   
                           |
| 66 | 1, 64, 65 | syl11anc 524 |
. . 3
       
                     
                                         |
| 67 | 66, 44, 51 | mpbi2and 801 |
. 2
    
   
                          |
| 68 | | df-sup 5664 |
. 2
     
        
 

   
          |
| 69 | 67, 68 | syl5eq 1940 |
1
        
           |