Metamath Proof Explorer

Theorem wlkoniswlk

Description: A walk between two vertices is a walk. (Contributed by Alexander van der Vekens, 12-Dec-2017) (Revised by AV, 2-Jan-2021)

Ref Expression
Assertion wlkoniswlk ⊢ F A WalksOn ⁡ G B P → F Walks ⁡ G P

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 wlkonprop ⊢ F A WalksOn ⁡ G B P → G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B
3 simp31 ⊢ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B → F Walks ⁡ G P
4 2 3 syl ⊢ F A WalksOn ⁡ G B P → F Walks ⁡ G P