Metamath Proof Explorer


Theorem crctisclwlk

Description: A circuit is a closed walk. (Contributed by AV, 17-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion crctisclwlk F Circuits G P F ClWalks G P

Proof

Step Hyp Ref Expression
1 crctprop F Circuits G P F Trails G P P 0 = P F
2 trliswlk F Trails G P F Walks G P
3 isclwlk F ClWalks G P F Walks G P P 0 = P F
4 3 biimpri F Walks G P P 0 = P F F ClWalks G P
5 2 4 sylan F Trails G P P 0 = P F F ClWalks G P
6 1 5 syl F Circuits G P F ClWalks G P