Theorem spthiswlk

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

	Ref	Expression
Assertion	spthiswlk	|- ( F ( SPaths ` G ) P -> F ( Walks ` G ) P )

Proof

Step	Hyp	Ref	Expression
1		spthispth	|- ( F ( SPaths ` G ) P -> F ( Paths ` G ) P )
2		pthiswlk	|- ( F ( Paths ` G ) P -> F ( Walks ` G ) P )
3	1 2	syl	|- ( F ( SPaths ` G ) P -> F ( Walks ` G ) P )