Metamath Proof Explorer

Theorem rusgrrgr

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

Ref Expression
Assertion rusgrrgr 
|- ( G RegUSGraph K -> G RegGraph K )

Proof

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