Metamath Proof Explorer

Theorem pthonispth

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

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