Metamath Proof Explorer

Theorem trlsonistrl

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

Ref Expression
Assertion trlsonistrl ⊢ F A TrailsOn ⁡ G B P → F Trails ⁡ G 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 simp3r ⊢ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A WalksOn ⁡ G B P ∧ F Trails ⁡ G P → F Trails ⁡ G P
4 2 3 syl ⊢ F A TrailsOn ⁡ G B P → F Trails ⁡ G P