Metamath Proof Explorer

Theorem pthontrlon

Description: A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021)

Ref Expression
Assertion pthontrlon ⊢ F A PathsOn ⁡ G B P → F A TrailsOn ⁡ G B P

Proof

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