Metamath Proof Explorer

Theorem clwwlkclwwlkn

Description: A closed walk of a fixed length as word is a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018) (Revised by AV, 24-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Assertion clwwlkclwwlkn ⊢ W ∈ N ClWWalksN G → W ∈ ClWWalks ⁡ G

Proof

Step Hyp Ref Expression
1 isclwwlkn ⊢ W ∈ N ClWWalksN G ↔ W ∈ ClWWalks ⁡ G ∧ W = N
2 1 simplbi ⊢ W ∈ N ClWWalksN G → W ∈ ClWWalks ⁡ G