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

Metamath Proof Explorer

Theorem ringgrpd

Description: A ring is a group. (Contributed by SN, 16-May-2024)

Ref Expression
Hypothesis ringgrpd.1 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion ringgrpd ( 𝜑 → 𝑅 ∈ Grp )

Proof

Step Hyp Ref Expression
1 ringgrpd.1 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
2 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
3 1 2 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )