This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cusgrusgr

Description: A complete simple graph is a simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 1-Nov-2020)

Ref Expression
Assertion cusgrusgr ⊢ G ∈ ComplUSGraph → G ∈ USGraph

Proof

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