Metamath Proof Explorer

Theorem rusgrusgr

Description: A k-regular simple graph is a simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018) (Revised by AV, 18-Dec-2020)

Ref Expression
Assertion rusgrusgr 
|- ( G RegUSGraph K -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 rusgrprop 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ G RegGraph K ) )
2 1 simpld 
 |-  ( G RegUSGraph K -> G e. USGraph )