Metamath Proof Explorer

Theorem grpmgmd

Description: A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025)

Ref Expression
Hypothesis grpmgmd.g 
|- ( ph -> G e. Grp )
Assertion grpmgmd 
|- ( ph -> G e. Mgm )

Proof

Step Hyp Ref Expression
1 grpmgmd.g 
 |-  ( ph -> G e. Grp )
2 1 grpmndd 
 |-  ( ph -> G e. Mnd )
3 mndmgm 
 |-  ( G e. Mnd -> G e. Mgm )
4 2 3 syl 
 |-  ( ph -> G e. Mgm )