Metamath Proof Explorer

Theorem upgracycusgr

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

		Ref	Expression
	Assertion	upgracycusgr	$⊢ (G \in UPGraph \land G \in AcyclicGraph) \to G \in USGraph$

Step	Hyp	Ref	Expression
1		upgracycumgr	$⊢ (G \in UPGraph \land G \in AcyclicGraph) \to G \in UMGraph$
2		umgracycusgr	$⊢ (G \in UMGraph \land G \in AcyclicGraph) \to G \in USGraph$
3	1 2	sylancom	$⊢ (G \in UPGraph \land G \in AcyclicGraph) \to G \in USGraph$