Metamath Proof Explorer


Theorem wlkoniswlk

Description: A walk between two vertices is a walk. (Contributed by Alexander van der Vekens, 12-Dec-2017) (Revised by AV, 2-Jan-2021)

Ref Expression
Assertion wlkoniswlk FAWalksOnGBPFWalksGP

Proof

Step Hyp Ref Expression
1 eqid VtxG=VtxG
2 1 wlkonprop FAWalksOnGBPGVAVtxGBVtxGFVPVFWalksGPP0=APF=B
3 simp31 GVAVtxGBVtxGFVPVFWalksGPP0=APF=BFWalksGP
4 2 3 syl FAWalksOnGBPFWalksGP