Theorem usgrn2cycl

Description: In a simple graph there are no cycles with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017) (Revised by AV, 4-Feb-2021)

	Ref	Expression
Assertion	usgrn2cycl	$$⊢\left(G\in \mathrm{USGraph}\wedge F\mathrm{Cycles}\left(G\right)P\right)\to \left|F\right|\ne 2$$

Proof

Step	Hyp	Ref	Expression
1		usgruspgr	$$⊢G\in \mathrm{USGraph}\to G\in \mathrm{USHGraph}$$
2		cycliscrct	$$⊢F\mathrm{Cycles}\left(G\right)P\to F\mathrm{Circuits}\left(G\right)P$$
3		uspgrn2crct	$$⊢\left(G\in \mathrm{USHGraph}\wedge F\mathrm{Circuits}\left(G\right)P\right)\to \left|F\right|\ne 2$$
4	1 2 3	syl2an	$$⊢\left(G\in \mathrm{USGraph}\wedge F\mathrm{Cycles}\left(G\right)P\right)\to \left|F\right|\ne 2$$