Theorem upgracycusgr

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

	Ref	Expression
Assertion	upgracycusgr	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph ) → 𝐺 ∈ USGraph )

Proof

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