Step | Hyp | Ref
| Expression |
1 | | 2pthfrgrarn2 25817 |
. . 3
 FriendGrph  
                    |
2 | | necom 2696 |
. . . . . . . . . . . 12

  |
3 | | eldifsn 4088 |
. . . . . . . . . . . . 13
    

   |
4 | 3 | simplbi2com 639 |
. . . . . . . . . . . 12
 
       |
5 | 2, 4 | sylbi 200 |
. . . . . . . . . . 11
 
       |
6 | 5 | com12 31 |
. . . . . . . . . 10
         |
7 | 6 | adantl 473 |
. . . . . . . . 9
 
         |
8 | 7 | imp 436 |
. . . . . . . 8
  



     |
9 | | sneq 3969 |
. . . . . . . . . . . . 13
       |
10 | 9 | difeq2d 3540 |
. . . . . . . . . . . 12
           |
11 | | preq1 4042 |
. . . . . . . . . . . . . . . 16
         |
12 | 11 | eleq1d 2533 |
. . . . . . . . . . . . . . 15
    
      |
13 | 12 | anbi1d 719 |
. . . . . . . . . . . . . 14
                     |
14 | | neeq1 2705 |
. . . . . . . . . . . . . . 15
 
   |
15 | 14 | anbi1d 719 |
. . . . . . . . . . . . . 14
  
      |
16 | 13, 15 | anbi12d 725 |
. . . . . . . . . . . . 13
                             |
17 | 16 | rexbidv 2892 |
. . . . . . . . . . . 12
  
            
               |
18 | 10, 17 | raleqbidv 2987 |
. . . . . . . . . . 11
  
                 
      
               |
19 | 18 | rspcv 3132 |
. . . . . . . . . 10
  

                  
                     |
20 | 19 | adantr 472 |
. . . . . . . . 9
 
                      
                     |
21 | 20 | adantr 472 |
. . . . . . . 8
  


 

                        
               |
22 | | preq2 4043 |
. . . . . . . . . . . . 13
         |
23 | 22 | eleq1d 2533 |
. . . . . . . . . . . 12
           |
24 | 23 | anbi2d 718 |
. . . . . . . . . . 11
     
               |
25 | | neeq2 2706 |
. . . . . . . . . . . 12
 
   |
26 | 25 | anbi2d 718 |
. . . . . . . . . . 11
  
      |
27 | 24, 26 | anbi12d 725 |
. . . . . . . . . 10
             
         
     |
28 | 27 | rexbidv 2892 |
. . . . . . . . 9
  
           

         
     |
29 | 28 | rspcv 3132 |
. . . . . . . 8
            
            
               |
30 | 8, 21, 29 | sylsyld 57 |
. . . . . . 7
  


 

                                  |
31 | | 2pthfrgrarn 25816 |
. . . . . . . . . 10
 FriendGrph  
                |
32 | | necom 2696 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
33 | | eldifsn 4088 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    

   |
34 | 33 | simplbi2com 639 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
35 | 32, 34 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
       |
36 | 35 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
         |
37 | 36 | imp 436 |
. . . . . . . . . . . . . . . . . . . . . 22
  

       |
38 | | sneq 3969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
    |
39 | 38 | difeq2d 3540 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
40 | | preq1 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
41 | 40 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
42 | 41 | anbi1d 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                     |
43 | 42 | rexbidv 2892 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
                    |
44 | 39, 43 | raleqbidv 2987 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
             
      
  
        |
45 | 44 | rspcv 3132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

                    
  
        |
46 | 45 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                 
      
  
        |
47 | 46 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
  

  

                    
  
        |
48 | | preq2 4043 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
49 | 48 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
50 | 49 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     |
51 | 50 | rexbidv 2892 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
               
    |
52 | 51 | rspcv 3132 |
. . . . . . . . . . . . . . . . . . . . . 22
            
  
            
    |
53 | 37, 47, 52 | sylsyld 57 |
. . . . . . . . . . . . . . . . . . . . 21
  

  

              
  
        |
54 | | prcom 4041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
55 | 54 | eleq1i 2540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
     |
56 | | prcom 4041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
57 | 56 | eleq1i 2540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
     |
58 | 55, 57 | anbi12ci 712 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
           |
59 | | preq2 4043 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
60 | 59 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
      |
61 | | preq1 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
62 | 61 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
63 | | biidd 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
      |
64 | 60, 62, 63 | 3anbi123d 1365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                           |
65 | | biidd 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
      |
66 | | preq2 4043 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
67 | 66 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
68 | | preq1 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
69 | 68 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
      |
70 | 65, 67, 69 | 3anbi123d 1365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
                     |
71 | 64, 70 | rspc2ev 3149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   
         
         
   |
72 | 71 | 3expa 1231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  

  
          
         
   |
73 | 72 | expcom 442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
          

  
           |
74 | 73 | 3expib 1234 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            
 
  
         
     |
75 | 58, 74 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
 
  
         
     |
76 | 75 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
              



  
            |
77 | 76 | com13 82 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
              
   


  
            |
78 | 77 | rexlimdva 2871 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      
          

         
     |
79 | 78 | com13 82 |
. . . . . . . . . . . . . . . . . . . . 21
    
               

         
     |
80 | 53, 79 | syl9 72 |
. . . . . . . . . . . . . . . . . . . 20
  

     
   
 

             



  
             |
81 | 80 | exp31 615 |
. . . . . . . . . . . . . . . . . . 19
 
         
 

             



  
               |
82 | 81 | com24 89 |
. . . . . . . . . . . . . . . . . 18
     
   

  

               

         
        |
83 | 82 | adantr 472 |
. . . . . . . . . . . . . . . . 17
           

  

               

         
        |
84 | 83 | impcom 437 |
. . . . . . . . . . . . . . . 16
     
                         



  
              |
85 | 84 | com15 95 |
. . . . . . . . . . . . . . 15
                   
     
       

         
       |
86 | 85 | pm2.43i 48 |
. . . . . . . . . . . . . 14
 
  
                           

         
      |
87 | 86 | com12 31 |
. . . . . . . . . . . . 13
                  
     
       

         
      |
88 | 87 | adantr 472 |
. . . . . . . . . . . 12
 
                  
     
       

         
      |
89 | 88 | adantr 472 |
. . . . . . . . . . 11
  



 

             
     
       

         
      |
90 | 89 | com4t 87 |
. . . . . . . . . 10
 

             
     
             

         
      |
91 | 31, 90 | syl 17 |
. . . . . . . . 9
 FriendGrph      
    
        

         
      |
92 | 91 | com14 90 |
. . . . . . . 8
                    FriendGrph


  
             |
93 | 92 | rexlimiv 2867 |
. . . . . . 7
      
             FriendGrph


  
            |
94 | 30, 93 | syl6 33 |
. . . . . 6
  


 

                    


 FriendGrph  
         
      |
95 | 94 | pm2.43a 50 |
. . . . 5
  


 

                   FriendGrph 

         
     |
96 | 95 | ex 441 |
. . . 4
 
                       
FriendGrph 

  
             |
97 | 96 | com4t 87 |
. . 3
 

                   FriendGrph     

  
             |
98 | 1, 97 | mpcom 36 |
. 2
 FriendGrph     

  
            |
99 | 98 | 3imp 1224 |
1
  FriendGrph





  
          |