Theorem mndmgm 18723

Description: A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.)

Assertion

Ref	Expression
mndmgm	⊢ (𝑀 ∈ Mnd → 𝑀 ∈ Mgm)

Proof of Theorem mndmgm

Step	Hyp	Ref	Expression
1		mndsgrp 18722	. 2 ⊢ (𝑀 ∈ Mnd → 𝑀 ∈ Smgrp)
2		sgrpmgm 18706	. 2 ⊢ (𝑀 ∈ Smgrp → 𝑀 ∈ Mgm)
3	1, 2	syl 17	1 ⊢ (𝑀 ∈ Mnd → 𝑀 ∈ Mgm)

Syntax hints:   → wi 4   ∈ wcel 2107  Mgmcmgm 18620  Smgrpcsgrp 18700  Mndcmnd 18716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-nul 5286

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-ov 7416  df-sgrp 18701  df-mnd 18717

This theorem is referenced by:  mndcl  18724  mndplusf  18734  ismhm0  18772  mhmismgmhm  18773  mndissubm  18789  grpmgmd  18948  grpissubg  19133  srg1zr  20180  ringmgm  20209  c0mgm  20427  c0snmgmhm  20430  c0snmhm  20431  psdmplcl  22114  psdadd  22115  psdpw  22122  chfacfpmmulgsum2  22819  cayhamlem1  22820  idomrootle  26148  fidomncyc  42508