Metamath Proof Explorer


Theorem drngringd

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

Ref Expression
Hypothesis drngringd.1 ( 𝜑𝑅 ∈ DivRing )
Assertion drngringd ( 𝜑𝑅 ∈ Ring )

Proof

Step Hyp Ref Expression
1 drngringd.1 ( 𝜑𝑅 ∈ DivRing )
2 drngring ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
3 1 2 syl ( 𝜑𝑅 ∈ Ring )