Metamath Proof Explorer


Theorem tdrgring

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

Ref Expression
Assertion tdrgring RTopDRingRRing

Proof

Step Hyp Ref Expression
1 tdrgtrg RTopDRingRTopRing
2 trgring RTopRingRRing
3 1 2 syl RTopDRingRRing