Metamath Proof Explorer


Theorem pthiswlk

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

Ref Expression
Assertion pthiswlk F Paths G P F Walks G P

Proof

Step Hyp Ref Expression
1 pthistrl F Paths G P F Trails G P
2 trliswlk F Trails G P F Walks G P
3 1 2 syl F Paths G P F Walks G P