Metamath Proof Explorer


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 G USGraph F Cycles G P F 2

Proof

Step Hyp Ref Expression
1 usgruspgr G USGraph G USHGraph
2 cycliscrct F Cycles G P F Circuits G P
3 uspgrn2crct G USHGraph F Circuits G P F 2
4 1 2 3 syl2an G USGraph F Cycles G P F 2