Step | Hyp | Ref
| Expression |
1 | | frisusgra 25720 |
. . . 4
 FriendGrph USGrph
  |
2 | | 4cycl4dv4e 25396 |
. . . . . . . 8
  USGrph
  Cycles         


                            |
3 | | frisusgrapr 25719 |
. . . . . . . . . . . . 13
 FriendGrph  USGrph  
                  |
4 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
5 | 4 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
  


    |
6 | 5 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
     
 
                          
  |
7 | | necom 2677 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
8 | 7 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . . 21
   |
9 | 8 | 3ad2ant2 1030 |
. . . . . . . . . . . . . . . . . . . 20
     |
10 | 9 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . 19
                     


     |
11 | 10 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
     
 
                          
  |
12 | | eldifsn 4097 |
. . . . . . . . . . . . . . . . . 18
     
   |
13 | 6, 11, 12 | sylanbrc 670 |
. . . . . . . . . . . . . . . . 17
     
 
                          

     |
14 | | sneq 3978 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
15 | 14 | difeq2d 3551 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
16 | | preq2 4052 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
17 | 16 | preq1d 4057 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     |
18 | 17 | sseq1d 3459 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
        
   |
19 | 18 | reubidv 2975 |
. . . . . . . . . . . . . . . . . . . . . 22
  
        
             |
20 | 15, 19 | raleqbidv 3001 |
. . . . . . . . . . . . . . . . . . . . 21
  
               
                  |
21 | 20 | rspcv 3146 |
. . . . . . . . . . . . . . . . . . . 20
  

                     
            |
22 | 21 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
                  
                   |
23 | 22 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
  


                   
                   |
24 | 23 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     
 
                          
 

              
                   |
25 | | preq2 4052 |
. . . . . . . . . . . . . . . . . . . . 21
         |
26 | 25 | preq2d 4058 |
. . . . . . . . . . . . . . . . . . . 20
                     |
27 | 26 | sseq1d 3459 |
. . . . . . . . . . . . . . . . . . 19
          
        
   |
28 | 27 | reubidv 2975 |
. . . . . . . . . . . . . . . . . 18
  
        
             |
29 | 28 | rspcv 3146 |
. . . . . . . . . . . . . . . . 17
                     

            |
30 | 13, 24, 29 | sylsyld 58 |
. . . . . . . . . . . . . . . 16
     
 
                          
 

              

            |
31 | | prcom 4050 |
. . . . . . . . . . . . . . . . . . . 20
       |
32 | 31 | preq1i 4054 |
. . . . . . . . . . . . . . . . . . 19
             
     |
33 | 32 | sseq1i 3456 |
. . . . . . . . . . . . . . . . . 18
         
        
  |
34 | 33 | reubii 2977 |
. . . . . . . . . . . . . . . . 17
          
     
      |
35 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . 21
                  
          |
36 | 35 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . 20
     
 
                          
          |
37 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
                  
          |
38 | 37 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . 20
     
 
                          
          |
39 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
40 | 39 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
  


    |
41 | 40 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     
 
                          
  |
42 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
43 | 42 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
  


    |
44 | 43 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     
 
                          
  |
45 | | simprr2 1057 |
. . . . . . . . . . . . . . . . . . . . 21
                     


     |
46 | 45 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
     
 
                          
  |
47 | | 4cycl2vnunb 25745 |
. . . . . . . . . . . . . . . . . . . 20
                          
      |
48 | 36, 38, 41, 44, 46, 47 | syl113anc 1280 |
. . . . . . . . . . . . . . . . . . 19
     
 
                          

    
      |
49 | 48 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . 18
     
 
                          
 
    
   
       |
50 | 49 | com12 32 |
. . . . . . . . . . . . . . . . 17
      
   
     
 
                          
       |
51 | 34, 50 | sylbi 199 |
. . . . . . . . . . . . . . . 16
          
     
 
                          
       |
52 | 30, 51 | syl6 34 |
. . . . . . . . . . . . . . 15
     
 
                          
 

              
     
 
                          
        |
53 | 52 | pm2.43b 52 |
. . . . . . . . . . . . . 14
 

              
     
 
                          
       |
54 | 53 | adantl 468 |
. . . . . . . . . . . . 13
  USGrph

                    
 
                      


   
       |
55 | 3, 54 | syl 17 |
. . . . . . . . . . . 12
 FriendGrph    


                            
       |
56 | 55 | com12 32 |
. . . . . . . . . . 11
     
 
                          
 FriendGrph        |
57 | 56 | ex 436 |
. . . . . . . . . 10
  


            
                 FriendGrph         |
58 | 57 | rexlimdvva 2886 |
. . . . . . . . 9
 
             
                 FriendGrph         |
59 | 58 | rexlimivv 2884 |
. . . . . . . 8
  


                    


    FriendGrph        |
60 | 2, 59 | syl 17 |
. . . . . . 7
  USGrph
  Cycles         FriendGrph        |
61 | 60 | 3exp 1207 |
. . . . . 6
 USGrph    Cycles         FriendGrph          |
62 | 61 | com34 86 |
. . . . 5
 USGrph    Cycles    FriendGrph               |
63 | 62 | com23 81 |
. . . 4
 USGrph  FriendGrph    Cycles                 |
64 | 1, 63 | mpcom 37 |
. . 3
 FriendGrph    Cycles                |
65 | 64 | imp 431 |
. 2
  FriendGrph
  Cycles   
    
       |
66 | | df-ne 2624 |
. . 3
    
      |
67 | 66 | biimpri 210 |
. 2
           |
68 | 65, 67 | pm2.61d1 163 |
1
  FriendGrph
  Cycles   
      |