Step | Hyp | Ref
| Expression |
1 | | frgrawopreg.a |
. . . 4
   VDeg       |
2 | | frgrawopreg.b |
. . . 4
   |
3 | 1, 2 | frgrawopreglem1 25772 |
. . 3
 FriendGrph 
   |
4 | | hashgt12el 12595 |
. . . . . . . . 9
       

  |
5 | 4 | ex 436 |
. . . . . . . 8
 
   


   |
6 | 5 | ad2antrr 732 |
. . . . . . 7
   
          

   |
7 | 6 | imp 431 |
. . . . . 6
   

          

  |
8 | | hashgt12el 12595 |
. . . . . . . 8
       

  |
9 | 8 | adantll 720 |
. . . . . . 7
   
     

  |
10 | 9 | adantr 467 |
. . . . . 6
   

          

  |
11 | | reeanv 2958 |
. . . . . . 7
  
 


 



   |
12 | | reeanv 2958 |
. . . . . . . . 9
  
 
 

   |
13 | 12 | 2rexbii 2890 |
. . . . . . . 8
  


 


 

   |
14 | | rexcom 2952 |
. . . . . . . . . . 11
  

 



    |
15 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
      FriendGrph
           |
16 | 15 | ancomd 453 |
. . . . . . . . . . . . . . . 16
      FriendGrph
           |
17 | 1, 2 | frgrawopreglem4 25775 |
. . . . . . . . . . . . . . . . . . . . . . 23
 FriendGrph  
     |
18 | | rsp2 2762 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

            |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 FriendGrph          |
20 | 19 | expdimp 439 |
. . . . . . . . . . . . . . . . . . . . 21
  FriendGrph
        |
21 | 20 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
   FriendGrph



      |
22 | 21 | imp 431 |
. . . . . . . . . . . . . . . . . . 19
    FriendGrph


      |
23 | 22 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
     FriendGrph 
        |
24 | 1, 2 | frgrawopreglem4 25775 |
. . . . . . . . . . . . . . . . . . . . . . 23
 FriendGrph  
     |
25 | | preq1 4051 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
26 | 25 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
27 | | preq2 4052 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
28 | 27 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
29 | 26, 28 | cbvral2v 3027 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  


     |
30 | | rsp2 2762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

            |
31 | 29, 30 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

            |
32 | 24, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 FriendGrph          |
33 | 32 | expd 438 |
. . . . . . . . . . . . . . . . . . . . 21
 FriendGrph 

       |
34 | 33 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
  FriendGrph
          |
35 | 34 | imp31 434 |
. . . . . . . . . . . . . . . . . . 19
    FriendGrph


      |
36 | 35 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
     FriendGrph 
        |
37 | 23, 36 | jca 535 |
. . . . . . . . . . . . . . . . 17
     FriendGrph 
             |
38 | 37 | adantr 467 |
. . . . . . . . . . . . . . . 16
      FriendGrph
                 |
39 | 1, 2 | frgrawopreglem4 25775 |
. . . . . . . . . . . . . . . . . . . . . 22
 FriendGrph  
     |
40 | | rsp2 2762 |
. . . . . . . . . . . . . . . . . . . . . 22
 

            |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 FriendGrph          |
42 | 41 | expdimp 439 |
. . . . . . . . . . . . . . . . . . . 20
  FriendGrph
        |
43 | 42 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . 19
    FriendGrph


        |
44 | 43 | imp 431 |
. . . . . . . . . . . . . . . . . 18
     FriendGrph 
        |
45 | | preq2 4052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
46 | 45 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
47 | 26, 46 | cbvral2v 3027 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

  


     |
48 | | rsp2 2762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

            |
49 | 47, 48 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

            |
50 | 24, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 FriendGrph          |
51 | 50 | expd 438 |
. . . . . . . . . . . . . . . . . . . . . 22
 FriendGrph 

       |
52 | 51 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
  FriendGrph
          |
53 | 52 | imp 431 |
. . . . . . . . . . . . . . . . . . . 20
   FriendGrph



      |
54 | 53 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
    FriendGrph


        |
55 | 54 | imp 431 |
. . . . . . . . . . . . . . . . . 18
     FriendGrph 
        |
56 | 44, 55 | jca 535 |
. . . . . . . . . . . . . . . . 17
     FriendGrph 
             |
57 | 56 | adantr 467 |
. . . . . . . . . . . . . . . 16
      FriendGrph
                 |
58 | 16, 38, 57 | 3jca 1188 |
. . . . . . . . . . . . . . 15
      FriendGrph
                 
           |
59 | 58 | ex 436 |
. . . . . . . . . . . . . 14
     FriendGrph 
    

          
            |
60 | 59 | reximdva 2862 |
. . . . . . . . . . . . 13
    FriendGrph


  



          
            |
61 | 60 | reximdva 2862 |
. . . . . . . . . . . 12
   FriendGrph


 

  

          
            |
62 | 61 | reximdva 2862 |
. . . . . . . . . . 11
  FriendGrph
  







          
            |
63 | 14, 62 | syl5bi 221 |
. . . . . . . . . 10
  FriendGrph
  







          
            |
64 | 63 | reximdva 2862 |
. . . . . . . . 9
 FriendGrph  



  



          
            |
65 | 64 | com12 32 |
. . . . . . . 8
  


  
FriendGrph 



          
            |
66 | 13, 65 | sylbir 217 |
. . . . . . 7
  
 

  FriendGrph




          
            |
67 | 11, 66 | sylbir 217 |
. . . . . 6
   


  FriendGrph




          
            |
68 | 7, 10, 67 | syl2anc 667 |
. . . . 5
   

           FriendGrph




          
            |
69 | 68 | exp31 609 |
. . . 4
 
           
FriendGrph 



          
              |
70 | 69 | com24 90 |
. . 3
 
  FriendGrph
     
   




          
              |
71 | 3, 70 | mpcom 37 |
. 2
 FriendGrph            


          
             |
72 | 71 | 3imp 1202 |
1
  FriendGrph
   
    




          
           |