Metamath Proof Explorer

Theorem spthonisspth

Description: A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 18-Jan-2021)

Ref Expression
Assertion spthonisspth ⊢ F A SPathsOn ⁡ G B P → F SPaths ⁡ G P

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 1 spthonprop ⊢ F A SPathsOn ⁡ G B P → G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P
3 simp3r ⊢ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ F ∈ V ∧ P ∈ V ∧ F A TrailsOn ⁡ G B P ∧ F SPaths ⁡ G P → F SPaths ⁡ G P
4 2 3 syl ⊢ F A SPathsOn ⁡ G B P → F SPaths ⁡ G P