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