Step | Hyp | Ref
| Expression |
1 | | grprcan.1 |
. . . . . . . 8
 |
2 | | eqid 2451 |
. . . . . . . 8
GId  GId   |
3 | 1, 2 | grpoidinv2 25946 |
. . . . . . 7
      GId        GId    
     GId      GId      |
4 | | simpr 463 |
. . . . . . . . 9
      GId      GId  
    GId    |
5 | 4 | reximi 2855 |
. . . . . . . 8
       GId      GId  

    GId    |
6 | 5 | adantl 468 |
. . . . . . 7
    GId        GId    
     GId      GId    
    GId    |
7 | 3, 6 | syl 17 |
. . . . . 6
   
    GId    |
8 | 7 | ad2ant2rl 755 |
. . . . 5
       
    GId    |
9 | | oveq1 6297 |
. . . . . . . . . . . 12
                           |
10 | 9 | ad2antll 735 |
. . . . . . . . . . 11
    

            
                  |
11 | 1 | grpoass 25931 |
. . . . . . . . . . . . . 14
  
 
                  |
12 | 11 | 3anassrs 1232 |
. . . . . . . . . . . . 13
    
                    |
13 | 12 | adantlrl 726 |
. . . . . . . . . . . 12
    

 
                   |
14 | 13 | adantrr 723 |
. . . . . . . . . . 11
    

            
                  |
15 | 1 | grpoass 25931 |
. . . . . . . . . . . . . . 15
  
 
                  |
16 | 15 | 3exp2 1227 |
. . . . . . . . . . . . . 14


                       |
17 | 16 | imp42 599 |
. . . . . . . . . . . . 13
   
                     |
18 | 17 | adantllr 725 |
. . . . . . . . . . . 12
    

 
                   |
19 | 18 | adantrr 723 |
. . . . . . . . . . 11
    

            
                  |
20 | 10, 14, 19 | 3eqtr3d 2493 |
. . . . . . . . . 10
    

            
                  |
21 | 20 | adantrrl 730 |
. . . . . . . . 9
    

        GId            
                  |
22 | | oveq2 6298 |
. . . . . . . . . . 11
     GId 
           GId     |
23 | 22 | ad2antrl 734 |
. . . . . . . . . 10
       GId                       GId     |
24 | 23 | adantl 468 |
. . . . . . . . 9
    

        GId            
           GId     |
25 | | oveq2 6298 |
. . . . . . . . . . 11
     GId 
           GId     |
26 | 25 | ad2antrl 734 |
. . . . . . . . . 10
       GId                       GId     |
27 | 26 | adantl 468 |
. . . . . . . . 9
    

        GId            
           GId     |
28 | 21, 24, 27 | 3eqtr3d 2493 |
. . . . . . . 8
    

        GId            
   GId      GId     |
29 | 1, 2 | grporid 25948 |
. . . . . . . . 9
      GId     |
30 | 29 | ad2antrr 732 |
. . . . . . . 8
    

        GId            
   GId     |
31 | 1, 2 | grporid 25948 |
. . . . . . . . . 10
      GId     |
32 | 31 | ad2ant2r 753 |
. . . . . . . . 9
          GId     |
33 | 32 | adantr 467 |
. . . . . . . 8
    

        GId            
   GId     |
34 | 28, 30, 33 | 3eqtr3d 2493 |
. . . . . . 7
    

        GId            
  |
35 | 34 | exp45 619 |
. . . . . 6
             GId                |
36 | 35 | rexlimdv 2877 |
. . . . 5
             GId               |
37 | 8, 36 | mpd 15 |
. . . 4
                   |
38 | | oveq1 6297 |
. . . 4
           |
39 | 37, 38 | impbid1 207 |
. . 3
                   |
40 | 39 | exp43 617 |
. 2


 
        
      |
41 | 40 | 3imp2 1224 |
1
  
 
        
   |