Theorem grpmgmd

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

	Ref	Expression
Hypothesis	grpmgmd.g	$$⊢\phi \to G\in \mathrm{Grp}$$
Assertion	grpmgmd	$$⊢\phi \to G\in \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		grpmgmd.g	$$⊢\phi \to G\in \mathrm{Grp}$$
2	1	grpmndd	$$⊢\phi \to G\in \mathrm{Mnd}$$
3		mndmgm	$$⊢G\in \mathrm{Mnd}\to G\in \mathrm{Mgm}$$
4	2 3	syl	$$⊢\phi \to G\in \mathrm{Mgm}$$