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