Metamath Proof Explorer

Theorem erclwwlkntr

Description: .~ is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Hypotheses erclwwlkn.w 
|- W = ( N ClWWalksN G )
erclwwlkn.r 
|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion erclwwlkntr 
|- ( ( x .~ y /\ y .~ z ) -> x .~ z )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w 
 |-  W = ( N ClWWalksN G )
2 erclwwlkn.r 
 |-  .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3 vex 
 |-  x e. _V
4 vex 
 |-  y e. _V
5 vex 
 |-  z e. _V
6 1 2 erclwwlkneqlen 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y -> ( # ` x ) = ( # ` y ) ) )
7 6 3adant3 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( # ` x ) = ( # ` y ) ) )
8 1 2 erclwwlkneqlen 
 |-  ( ( y e. _V /\ z e. _V ) -> ( y .~ z -> ( # ` y ) = ( # ` z ) ) )
9 8 3adant1 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z -> ( # ` y ) = ( # ` z ) ) )
10 1 2 erclwwlkneq 
 |-  ( ( y e. _V /\ z e. _V ) -> ( y .~ z <-> ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) )
11 10 3adant1 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z <-> ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) )
12 1 2 erclwwlkneq 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y <-> ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) )
13 12 3adant3 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y <-> ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) )
14 simpr1 
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) /\ ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) -> x e. W )
15 simplr2 
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) /\ ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) -> z e. W )
16 oveq2 
 |-  ( n = m -> ( y cyclShift n ) = ( y cyclShift m ) )
17 16 eqeq2d 
 |-  ( n = m -> ( x = ( y cyclShift n ) <-> x = ( y cyclShift m ) ) )
18 17 cbvrexvw 
 |-  ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) <-> E. m e. ( 0 ... N ) x = ( y cyclShift m ) )
19 oveq2 
 |-  ( n = k -> ( z cyclShift n ) = ( z cyclShift k ) )
20 19 eqeq2d 
 |-  ( n = k -> ( y = ( z cyclShift n ) <-> y = ( z cyclShift k ) ) )
21 20 cbvrexvw 
 |-  ( E. n e. ( 0 ... N ) y = ( z cyclShift n ) <-> E. k e. ( 0 ... N ) y = ( z cyclShift k ) )
22 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
23 22 clwwlknbp 
 |-  ( z e. ( N ClWWalksN G ) -> ( z e. Word ( Vtx ` G ) /\ ( # ` z ) = N ) )
24 eqcom 
 |-  ( ( # ` z ) = N <-> N = ( # ` z ) )
25 24 biimpi 
 |-  ( ( # ` z ) = N -> N = ( # ` z ) )
26 23 25 simpl2im 
 |-  ( z e. ( N ClWWalksN G ) -> N = ( # ` z ) )
27 26 1 eleq2s 
 |-  ( z e. W -> N = ( # ` z ) )
28 27 ad2antlr 
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> N = ( # ` z ) )
29 23 simpld 
 |-  ( z e. ( N ClWWalksN G ) -> z e. Word ( Vtx ` G ) )
30 29 1 eleq2s 
 |-  ( z e. W -> z e. Word ( Vtx ` G ) )
31 30 ad2antlr 
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> z e. Word ( Vtx ` G ) )
32 31 adantl 
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> z e. Word ( Vtx ` G ) )
33 simprr 
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) )
34 32 33 cshwcsh2id 
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
35 oveq2 
 |-  ( N = ( # ` z ) -> ( 0 ... N ) = ( 0 ... ( # ` z ) ) )
36 oveq2 
 |-  ( ( # ` z ) = ( # ` y ) -> ( 0 ... ( # ` z ) ) = ( 0 ... ( # ` y ) ) )
37 36 eqcoms 
 |-  ( ( # ` y ) = ( # ` z ) -> ( 0 ... ( # ` z ) ) = ( 0 ... ( # ` y ) ) )
38 37 adantr 
 |-  ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( 0 ... ( # ` z ) ) = ( 0 ... ( # ` y ) ) )
39 38 adantl 
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( 0 ... ( # ` z ) ) = ( 0 ... ( # ` y ) ) )
40 35 39 sylan9eq 
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( 0 ... N ) = ( 0 ... ( # ` y ) ) )
41 40 eleq2d 
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( m e. ( 0 ... N ) <-> m e. ( 0 ... ( # ` y ) ) ) )
42 41 anbi1d 
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( m e. ( 0 ... N ) /\ x = ( y cyclShift m ) ) <-> ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) ) )
43 35 eleq2d 
 |-  ( N = ( # ` z ) -> ( k e. ( 0 ... N ) <-> k e. ( 0 ... ( # ` z ) ) ) )
44 43 anbi1d 
 |-  ( N = ( # ` z ) -> ( ( k e. ( 0 ... N ) /\ y = ( z cyclShift k ) ) <-> ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) )
45 44 adantr 
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( k e. ( 0 ... N ) /\ y = ( z cyclShift k ) ) <-> ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) )
46 42 45 anbi12d 
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( ( m e. ( 0 ... N ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... N ) /\ y = ( z cyclShift k ) ) ) <-> ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) ) )
47 35 rexeqdv 
 |-  ( N = ( # ` z ) -> ( E. n e. ( 0 ... N ) x = ( z cyclShift n ) <-> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
48 47 adantr 
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( E. n e. ( 0 ... N ) x = ( z cyclShift n ) <-> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
49 34 46 48 3imtr4d 
 |-  ( ( N = ( # ` z ) /\ ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) ) -> ( ( ( m e. ( 0 ... N ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... N ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
50 28 49 mpancom 
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( ( ( m e. ( 0 ... N ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... N ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
51 50 exp5l 
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( m e. ( 0 ... N ) -> ( x = ( y cyclShift m ) -> ( k e. ( 0 ... N ) -> ( y = ( z cyclShift k ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) ) ) )
52 51 imp41 
 |-  ( ( ( ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) /\ m e. ( 0 ... N ) ) /\ x = ( y cyclShift m ) ) /\ k e. ( 0 ... N ) ) -> ( y = ( z cyclShift k ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
53 52 rexlimdva 
 |-  ( ( ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) /\ m e. ( 0 ... N ) ) /\ x = ( y cyclShift m ) ) -> ( E. k e. ( 0 ... N ) y = ( z cyclShift k ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
54 53 ex 
 |-  ( ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) /\ m e. ( 0 ... N ) ) -> ( x = ( y cyclShift m ) -> ( E. k e. ( 0 ... N ) y = ( z cyclShift k ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
55 54 rexlimdva 
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( E. m e. ( 0 ... N ) x = ( y cyclShift m ) -> ( E. k e. ( 0 ... N ) y = ( z cyclShift k ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
56 21 55 syl7bi 
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( E. m e. ( 0 ... N ) x = ( y cyclShift m ) -> ( E. n e. ( 0 ... N ) y = ( z cyclShift n ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
57 18 56 syl5bi 
 |-  ( ( ( ( x e. W /\ y e. W ) /\ z e. W ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( E. n e. ( 0 ... N ) y = ( z cyclShift n ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
58 57 exp31 
 |-  ( ( x e. W /\ y e. W ) -> ( z e. W -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( E. n e. ( 0 ... N ) y = ( z cyclShift n ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) ) ) )
59 58 com15 
 |-  ( E. n e. ( 0 ... N ) y = ( z cyclShift n ) -> ( z e. W -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( x e. W /\ y e. W ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) ) ) )
60 59 impcom 
 |-  ( ( z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( x e. W /\ y e. W ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) ) )
61 60 3adant1 
 |-  ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( x e. W /\ y e. W ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) ) )
62 61 impcom 
 |-  ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( x e. W /\ y e. W ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
63 62 com13 
 |-  ( ( x e. W /\ y e. W ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
64 63 3impia 
 |-  ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
65 64 impcom 
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) /\ ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) -> E. n e. ( 0 ... N ) x = ( z cyclShift n ) )
66 14 15 65 3jca 
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) /\ ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) -> ( x e. W /\ z e. W /\ E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) )
67 1 2 erclwwlkneq 
 |-  ( ( x e. _V /\ z e. _V ) -> ( x .~ z <-> ( x e. W /\ z e. W /\ E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
68 67 3adant2 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ z <-> ( x e. W /\ z e. W /\ E. n e. ( 0 ... N ) x = ( z cyclShift n ) ) ) )
69 66 68 syl5ibrcom 
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) ) /\ ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> x .~ z ) )
70 69 exp31 
 |-  ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> x .~ z ) ) ) )
71 70 com24 
 |-  ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) )
72 71 ex 
 |-  ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) ) )
73 72 com4t 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) ) )
74 13 73 sylbid 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) ) )
75 74 com25 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( y e. W /\ z e. W /\ E. n e. ( 0 ... N ) y = ( z cyclShift n ) ) -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( x .~ y -> x .~ z ) ) ) ) )
76 11 75 sylbid 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( x .~ y -> x .~ z ) ) ) ) )
77 9 76 mpdd 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z -> ( ( # ` x ) = ( # ` y ) -> ( x .~ y -> x .~ z ) ) ) )
78 77 com24 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( ( # ` x ) = ( # ` y ) -> ( y .~ z -> x .~ z ) ) ) )
79 7 78 mpdd 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( y .~ z -> x .~ z ) ) )
80 79 impd 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x .~ y /\ y .~ z ) -> x .~ z ) )
81 3 4 5 80 mp3an 
 |-  ( ( x .~ y /\ y .~ z ) -> x .~ z )