Metamath Proof Explorer


Theorem ringmgm

Description: A ring is a magma. (Contributed by AV, 31-Jan-2020)

Ref Expression
Assertion ringmgm R Ring R Mgm

Proof

Step Hyp Ref Expression
1 ringmnd R Ring R Mnd
2 mndmgm R Mnd R Mgm
3 1 2 syl R Ring R Mgm