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	$$⊢\left(G\in \mathrm{USGraph}\wedge \left|F\right|=2\right)\to \left(F\mathrm{Paths}\left(G\right)P\leftrightarrow F\mathrm{SPaths}\left(G\right)P\right)$$

Proof

Step	Hyp	Ref	Expression
1		pthistrl	$$⊢F\mathrm{Paths}\left(G\right)P\to F\mathrm{Trails}\left(G\right)P$$
2		usgr2trlspth	$$⊢\left(G\in \mathrm{USGraph}\wedge \left|F\right|=2\right)\to \left(F\mathrm{Trails}\left(G\right)P\leftrightarrow F\mathrm{SPaths}\left(G\right)P\right)$$
3	1 2	syl5ib	$$⊢\left(G\in \mathrm{USGraph}\wedge \left|F\right|=2\right)\to \left(F\mathrm{Paths}\left(G\right)P\to F\mathrm{SPaths}\left(G\right)P\right)$$
4		spthispth	$$⊢F\mathrm{SPaths}\left(G\right)P\to F\mathrm{Paths}\left(G\right)P$$
5	3 4	impbid1	$$⊢\left(G\in \mathrm{USGraph}\wedge \left|F\right|=2\right)\to \left(F\mathrm{Paths}\left(G\right)P\leftrightarrow F\mathrm{SPaths}\left(G\right)P\right)$$