Metamath Proof Explorer

Theorem upgracycusgr

Description: An acyclic pseudograph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023)

Ref Expression
Assertion upgracycusgr ⊢ G ∈ UPGraph ∧ G ∈ AcyclicGraph → G ∈ USGraph

Proof

Step Hyp Ref Expression
1 upgracycumgr ⊢ G ∈ UPGraph ∧ G ∈ AcyclicGraph → G ∈ UMGraph
2 umgracycusgr ⊢ G ∈ UMGraph ∧ G ∈ AcyclicGraph → G ∈ USGraph
3 1 2 sylancom ⊢ G ∈ UPGraph ∧ G ∈ AcyclicGraph → G ∈ USGraph