Description: A division ring is a ring. (Contributed by SN, 16-May-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | drngringd.1 | ⊢ ( 𝜑 → 𝑅 ∈ DivRing ) | |
Assertion | drngringd | ⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | drngringd.1 | ⊢ ( 𝜑 → 𝑅 ∈ DivRing ) | |
2 | drngring | ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring ) | |
3 | 1 2 | syl | ⊢ ( 𝜑 → 𝑅 ∈ Ring ) |