Metamath Proof Explorer

Theorem tdrgtmd

Description: A topological division ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015)

		Ref	Expression
	Assertion	tdrgtmd	$⊢ R \in TopDRing \to R \in TopMnd$

Step	Hyp	Ref	Expression
1		tdrgtrg	$⊢ R \in TopDRing \to R \in TopRing$
2		trgtmd2	$⊢ R \in TopRing \to R \in TopMnd$
3	1 2	syl	$⊢ R \in TopDRing \to R \in TopMnd$