This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trggrp

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

Ref Expression
Assertion trggrp 
|- ( R e. TopRing -> R e. Grp )

Proof

Step Hyp Ref Expression
1 trgring 
 |-  ( R e. TopRing -> R e. Ring )
2 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
3 1 2 syl 
 |-  ( R e. TopRing -> R e. Grp )