Database
BASIC ALGEBRAIC STRUCTURES
Rings
Unital rings
ringmgm
Next ⟩
crngring
Metamath Proof Explorer
Ascii
Structured
Theorem
ringmgm
Description:
A ring is a magma.
(Contributed by
AV
, 31-Jan-2020)
Ref
Expression
Assertion
ringmgm
⊢
(
𝑅
∈ Ring →
𝑅
∈ Mgm )
Proof
Step
Hyp
Ref
Expression
1
ringmnd
⊢
(
𝑅
∈ Ring →
𝑅
∈ Mnd )
2
mndmgm
⊢
(
𝑅
∈ Mnd →
𝑅
∈ Mgm )
3
1
2
syl
⊢
(
𝑅
∈ Ring →
𝑅
∈ Mgm )