Database
GRAPH THEORY
Walks, paths and cycles
Paths and simple paths
pthiswlk
Next ⟩
spthiswlk
Metamath Proof Explorer
Ascii
Unicode
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