This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgr2pthspth

Description: In a simple graph, any path of length 2 is a simple path. (Contributed by Alexander van der Vekens, 25-Jan-2018) (Revised by AV, 5-Jun-2021)

Ref Expression
Assertion usgr2pthspth ⊢ G ∈ USGraph ∧ F = 2 → F Paths ⁡ G P ↔ F SPaths ⁡ G P

Proof

Step Hyp Ref Expression
1 pthistrl ⊢ F Paths ⁡ G P → F Trails ⁡ G P
2 usgr2trlspth ⊢ G ∈ USGraph ∧ F = 2 → F Trails ⁡ G P ↔ F SPaths ⁡ G P
3 1 2 imbitrid ⊢ G ∈ USGraph ∧ F = 2 → F Paths ⁡ G P → F SPaths ⁡ G P
4 spthispth ⊢ F SPaths ⁡ G P → F Paths ⁡ G P
5 3 4 impbid1 ⊢ G ∈ USGraph ∧ F = 2 → F Paths ⁡ G P ↔ F SPaths ⁡ G P