Step | Hyp | Ref
| Expression |
1 | | neirr 2644 |
. . . . . . . . . . . . . . . 16
 |
2 | | usgraedgrn 25157 |
. . . . . . . . . . . . . . . . 17
     USGrph    
  |
3 | 2 | ex 440 |
. . . . . . . . . . . . . . . 16
    USGrph        |
4 | 1, 3 | mtoi 183 |
. . . . . . . . . . . . . . 15
    USGrph
     |
5 | 4 | adantl 472 |
. . . . . . . . . . . . . 14
       
 USGrph 
     |
6 | 5 | intnanrd 933 |
. . . . . . . . . . . . 13
       
 USGrph 
     
    |
7 | | prex 4656 |
. . . . . . . . . . . . . 14
    |
8 | | prex 4656 |
. . . . . . . . . . . . . 14
    |
9 | 7, 8 | prss 4139 |
. . . . . . . . . . . . 13
    
   
      
    |
10 | 6, 9 | sylnib 310 |
. . . . . . . . . . . 12
       
 USGrph 
  
     
  |
11 | | neirr 2644 |
. . . . . . . . . . . . . . . 16
 |
12 | | usgraedgrn 25157 |
. . . . . . . . . . . . . . . . 17
     USGrph    
  |
13 | 12 | ex 440 |
. . . . . . . . . . . . . . . 16
    USGrph        |
14 | 11, 13 | mtoi 183 |
. . . . . . . . . . . . . . 15
    USGrph
     |
15 | 14 | adantl 472 |
. . . . . . . . . . . . . 14
       
 USGrph 
     |
16 | 15 | intnand 932 |
. . . . . . . . . . . . 13
       
 USGrph 
     
    |
17 | | prex 4656 |
. . . . . . . . . . . . . 14
    |
18 | | prex 4656 |
. . . . . . . . . . . . . 14
    |
19 | 17, 18 | prss 4139 |
. . . . . . . . . . . . 13
    
   
      
    |
20 | 16, 19 | sylnib 310 |
. . . . . . . . . . . 12
       
 USGrph 
  
     
  |
21 | | ioran 497 |
. . . . . . . . . . . 12
        
      
    
     
            
   |
22 | 10, 20, 21 | sylanbrc 675 |
. . . . . . . . . . 11
       
 USGrph 
     
      
     
   |
23 | | preq1 4064 |
. . . . . . . . . . . . . . 15
     
   |
24 | | preq1 4064 |
. . . . . . . . . . . . . . 15
     
   |
25 | 23, 24 | preq12d 4072 |
. . . . . . . . . . . . . 14
         
           |
26 | 25 | sseq1d 3471 |
. . . . . . . . . . . . 13
      
                |
27 | | preq1 4064 |
. . . . . . . . . . . . . . 15
     
   |
28 | | preq1 4064 |
. . . . . . . . . . . . . . 15
     
   |
29 | 27, 28 | preq12d 4072 |
. . . . . . . . . . . . . 14
         
           |
30 | 29 | sseq1d 3471 |
. . . . . . . . . . . . 13
      
                |
31 | 26, 30 | rexprg 4034 |
. . . . . . . . . . . 12
 
              
         
             |
32 | 31 | ad2antrr 737 |
. . . . . . . . . . 11
       
 USGrph 
 
           
            
     
    |
33 | 22, 32 | mtbird 307 |
. . . . . . . . . 10
       
 USGrph 
               |
34 | | reurex 3021 |
. . . . . . . . . 10
             
  
     
      |
35 | 33, 34 | nsyl 126 |
. . . . . . . . 9
       
 USGrph 

           
  |
36 | 35 | orcd 398 |
. . . . . . . 8
       
 USGrph 
 
           
                |
37 | | rexnal 2848 |
. . . . . . . . . . . 12
                     
    
                
  |
38 | 37 | bicomi 207 |
. . . . . . . . . . 11
                      
    
   
              |
39 | 38 | a1i 11 |
. . . . . . . . . 10
       
 USGrph 
            
     
   
                    
   |
40 | | difprsn1 4121 |
. . . . . . . . . . . 12
            |
41 | 40 | ad2antlr 738 |
. . . . . . . . . . 11
       
 USGrph 
  
        |
42 | 41 | rexeqdv 3006 |
. . . . . . . . . 10
       
 USGrph 
 
  
                
   
               |
43 | | preq2 4065 |
. . . . . . . . . . . . . . . 16
         |
44 | 43 | preq2d 4071 |
. . . . . . . . . . . . . . 15
              
      |
45 | 44 | sseq1d 3471 |
. . . . . . . . . . . . . 14
      
   
            |
46 | 45 | reubidv 2987 |
. . . . . . . . . . . . 13
  
              
     
       |
47 | 46 | notbid 300 |
. . . . . . . . . . . 12
    
     
   
                |
48 | 47 | rexsng 4019 |
. . . . . . . . . . 11
  
              

           
   |
49 | 48 | ad3antlr 742 |
. . . . . . . . . 10
       
 USGrph 
 
              

           
   |
50 | 39, 42, 49 | 3bitrd 287 |
. . . . . . . . 9
       
 USGrph 
            
     
   
                |
51 | | rexnal 2848 |
. . . . . . . . . . . 12
                     
    
                
  |
52 | 51 | bicomi 207 |
. . . . . . . . . . 11
                      
    
   
              |
53 | 52 | a1i 11 |
. . . . . . . . . 10
       
 USGrph 
            
     
   
                    
   |
54 | | difprsn2 4122 |
. . . . . . . . . . . 12
            |
55 | 54 | ad2antlr 738 |
. . . . . . . . . . 11
       
 USGrph 
  
        |
56 | 55 | rexeqdv 3006 |
. . . . . . . . . 10
       
 USGrph 
 
  
                
   
               |
57 | | preq2 4065 |
. . . . . . . . . . . . . . . 16
         |
58 | 57 | preq2d 4071 |
. . . . . . . . . . . . . . 15
              
      |
59 | 58 | sseq1d 3471 |
. . . . . . . . . . . . . 14
      
   
            |
60 | 59 | reubidv 2987 |
. . . . . . . . . . . . 13
  
              
     
       |
61 | 60 | notbid 300 |
. . . . . . . . . . . 12
    
     
   
                |
62 | 61 | rexsng 4019 |
. . . . . . . . . . 11
  
              

           
   |
63 | 62 | ad3antrrr 741 |
. . . . . . . . . 10
       
 USGrph 
 
              

           
   |
64 | 53, 56, 63 | 3bitrd 287 |
. . . . . . . . 9
       
 USGrph 
            
     
   
                |
65 | 50, 64 | orbi12d 721 |
. . . . . . . 8
       
 USGrph 
                       
                     
                 
     
        |
66 | 36, 65 | mpbird 240 |
. . . . . . 7
       
 USGrph 
            
     
   
           
     
       |
67 | | sneq 3990 |
. . . . . . . . . . . 12
       |
68 | 67 | difeq2d 3563 |
. . . . . . . . . . 11
                 |
69 | | preq2 4065 |
. . . . . . . . . . . . . 14
         |
70 | 69 | preq1d 4070 |
. . . . . . . . . . . . 13
              
      |
71 | 70 | sseq1d 3471 |
. . . . . . . . . . . 12
          
        
   |
72 | 71 | reubidv 2987 |
. . . . . . . . . . 11
  
              
     
       |
73 | 68, 72 | raleqbidv 3013 |
. . . . . . . . . 10
  
          
         
                     
   |
74 | 73 | notbid 300 |
. . . . . . . . 9
                       
    
                
   |
75 | | sneq 3990 |
. . . . . . . . . . . 12
       |
76 | 75 | difeq2d 3563 |
. . . . . . . . . . 11
                 |
77 | | preq2 4065 |
. . . . . . . . . . . . . 14
         |
78 | 77 | preq1d 4070 |
. . . . . . . . . . . . 13
              
      |
79 | 78 | sseq1d 3471 |
. . . . . . . . . . . 12
          
        
   |
80 | 79 | reubidv 2987 |
. . . . . . . . . . 11
  
              
     
       |
81 | 76, 80 | raleqbidv 3013 |
. . . . . . . . . 10
  
          
         
                     
   |
82 | 81 | notbid 300 |
. . . . . . . . 9
                       
    
                
   |
83 | 74, 82 | rexprg 4034 |
. . . . . . . 8
 
          
                
            
     
   
           
     
        |
84 | 83 | ad2antrr 737 |
. . . . . . 7
       
 USGrph 
 
   
  
       
         
 
  
       
     
   
           
     
        |
85 | 66, 84 | mpbird 240 |
. . . . . 6
       
 USGrph 
        
                
  |
86 | | rexnal 2848 |
. . . . . 6
     
  
       
         
                          
  |
87 | 85, 86 | sylib 201 |
. . . . 5
       
 USGrph 
                          
  |
88 | 87 | intnand 932 |
. . . 4
       
 USGrph 
    USGrph                           
   |
89 | | usgrav 25114 |
. . . . . 6
    USGrph        |
90 | 89 | adantl 472 |
. . . . 5
       
 USGrph 
  
    |
91 | | isfrgra 25767 |
. . . . 5
    
     FriendGrph    
USGrph 
        
                
    |
92 | 90, 91 | syl 17 |
. . . 4
       
 USGrph 
  
 FriendGrph    
USGrph 
        
                
    |
93 | 88, 92 | mtbird 307 |
. . 3
       
 USGrph 
  
FriendGrph   |
94 | 93 | expcom 441 |
. 2
    USGrph   


  
FriendGrph    |
95 | | frisusgra 25769 |
. . . 4
    FriendGrph   
USGrph   |
96 | 95 | con3i 142 |
. . 3
    USGrph
  
FriendGrph   |
97 | 96 | a1d 26 |
. 2
    USGrph
  


  
FriendGrph    |
98 | 94, 97 | pm2.61i 169 |
1
  


  
FriendGrph   |