Metamath Proof Explorer

Theorem trlsonwlkon

Description: A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017) (Revised by AV, 7-Jan-2021)

Ref Expression
Assertion trlsonwlkon ⊢ F A TrailsOn ⁡ G B P → F A WalksOn ⁡ G B P

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 trlsonprop ⊢ F A TrailsOn ⁡ G B P → G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P
3 simp3l ⊢ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P → F A WalksOn ⁡ G B P
4 2 3 syl ⊢ F A TrailsOn ⁡ G B P → F A WalksOn ⁡ G B P