Metamath Proof Explorer

Theorem ringmgm

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

Ref Expression
Assertion ringmgm 
|- ( R e. Ring -> R e. Mgm )

Proof

Step Hyp Ref Expression
1 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
2 mndmgm 
 |-  ( R e. Mnd -> R e. Mgm )
3 1 2 syl 
 |-  ( R e. Ring -> R e. Mgm )