Metamath Proof Explorer

Theorem usgrupgr

Description: A simple graph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 20-Aug-2017) (Revised by AV, 15-Oct-2020)

Ref Expression
Assertion usgrupgr ⊢ G ∈ USGraph → G ∈ UPGraph

Proof

Step Hyp Ref Expression
1 usgruspgr ⊢ G ∈ USGraph → G ∈ USHGraph
2 uspgrupgr ⊢ G ∈ USHGraph → G ∈ UPGraph
3 1 2 syl ⊢ G ∈ USGraph → G ∈ UPGraph