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 ∈ ComplUSGraph → G ∈ ComplGraph

Proof

Step Hyp Ref Expression
1 iscusgr ⊢ G ∈ ComplUSGraph ↔ G ∈ USGraph ∧ G ∈ ComplGraph
2 1 simprbi ⊢ G ∈ ComplUSGraph → G ∈ ComplGraph