Step | Hyp | Ref
| Expression |
1 | | df-rab 2746 |
. . 3
 Word   ..^       cyclShift     Word   ..^       cyclShift     |
2 | | r19.42v 2945 |
. . . . 5
   ..^       Word  cyclShift    Word   ..^       cyclShift     |
3 | 2 | bicomi 206 |
. . . 4
  Word   ..^       cyclShift     ..^       Word  cyclShift     |
4 | 3 | abbii 2567 |
. . 3
  Word   ..^       cyclShift       ..^       Word 
cyclShift     |
5 | | df-rex 2743 |
. . . 4
   ..^       Word  cyclShift       ..^    
 Word  cyclShift      |
6 | 5 | abbii 2567 |
. . 3
   ..^       Word  cyclShift         ..^      Word

cyclShift      |
7 | 1, 4, 6 | 3eqtri 2477 |
. 2
 Word   ..^       cyclShift        ..^    
 Word  cyclShift      |
8 | | abid2 2573 |
. . . 4

 ..^       ..^      |
9 | | ovex 6318 |
. . . 4
 ..^      |
10 | 8, 9 | eqeltri 2525 |
. . 3

 ..^       |
11 | | tru 1448 |
. . . . 5
 |
12 | 11, 11 | pm3.2i 457 |
. . . 4
 |
13 | | ovex 6318 |
. . . . . . 7
 cyclShift   |
14 | 13 | a1i 11 |
. . . . . 6
 cyclShift
   |
15 | | eqtr3 2472 |
. . . . . . . . . . . . 13
   cyclShift   cyclShift  
  |
16 | 15 | ex 436 |
. . . . . . . . . . . 12
  cyclShift    cyclShift
    |
17 | 16 | eqcoms 2459 |
. . . . . . . . . . 11
  cyclShift    cyclShift
    |
18 | 17 | adantl 468 |
. . . . . . . . . 10
  Word 
cyclShift     cyclShift     |
19 | 18 | com12 32 |
. . . . . . . . 9
  cyclShift    Word  cyclShift  
   |
20 | 19 | ad2antlr 733 |
. . . . . . . 8
   cyclShift     Word  cyclShift  
   |
21 | 20 | alrimiv 1773 |
. . . . . . 7
   cyclShift       Word 
cyclShift      |
22 | 21 | ex 436 |
. . . . . 6
  cyclShift
 
    Word 
cyclShift       |
23 | 14, 22 | spcimedv 3133 |
. . . . 5
      Word  cyclShift
      |
24 | 23 | imp 431 |
. . . 4
       Word  cyclShift  
   |
25 | 12, 24 | mp1i 13 |
. . 3
  ..^    
      Word  cyclShift  
   |
26 | 10, 25 | zfrep4 4523 |
. 2
     ..^    
 Word  cyclShift      |
27 | 7, 26 | eqeltri 2525 |
1
 Word   ..^       cyclShift    |