Metamath Proof Explorer


Theorem usgr2edg

Description: If a vertex is adjacent to two different vertices in a simple graph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 17-Oct-2020) (Proof shortened by AV, 11-Feb-2021)

Ref Expression
Hypotheses usgrf1oedg.i I=iEdgG
usgrf1oedg.e E=EdgG
Assertion usgr2edg GUSGraphABNAEBNExdomIydomIxyNIxNIy

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i I=iEdgG
2 usgrf1oedg.e E=EdgG
3 usgrumgr GUSGraphGUMGraph
4 1 2 umgr2edg GUMGraphABNAEBNExdomIydomIxyNIxNIy
5 3 4 sylanl1 GUSGraphABNAEBNExdomIydomIxyNIxNIy