Metamath Proof Explorer


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 )