Metamath Proof Explorer

Theorem upgracycusgr

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

Ref Expression
Assertion upgracycusgr 
|- ( ( G e. UPGraph /\ G e. AcyclicGraph ) -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 upgracycumgr 
 |-  ( ( G e. UPGraph /\ G e. AcyclicGraph ) -> G e. UMGraph )
2 umgracycusgr 
 |-  ( ( G e. UMGraph /\ G e. AcyclicGraph ) -> G e. USGraph )
3 1 2 sylancom 
 |-  ( ( G e. UPGraph /\ G e. AcyclicGraph ) -> G e. USGraph )