Metamath Proof Explorer


Theorem grpmgmd

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

Ref Expression
Hypothesis grpmgmd.g φGGrp
Assertion grpmgmd φGMgm

Proof

Step Hyp Ref Expression
1 grpmgmd.g φGGrp
2 1 grpmndd φGMnd
3 mndmgm GMndGMgm
4 2 3 syl φGMgm