Metamath Proof Explorer

Theorem cusgrcplgr

Description: A complete simple graph is a complete graph. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion cusgrcplgr 
|- ( G e. ComplUSGraph -> G e. ComplGraph )

Proof

Step Hyp Ref Expression
1 iscusgr 
 |-  ( G e. ComplUSGraph <-> ( G e. USGraph /\ G e. ComplGraph ) )
2 1 simprbi 
 |-  ( G e. ComplUSGraph -> G e. ComplGraph )