Theorem spthiswlk

Description: A simple path is a walk (in an undirected graph). (Contributed by AV, 16-May-2021)

	Ref	Expression
Assertion	spthiswlk	⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		spthispth	⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
2		pthiswlk	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
3	1 2	syl	⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )