Theorem mndmgm 18698

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 18697	. 2 ⊢ (𝑀 ∈ Mnd → 𝑀 ∈ Smgrp)
2		sgrpmgm 18681	. 2 ⊢ (𝑀 ∈ Smgrp → 𝑀 ∈ Mgm)
3	1, 2	syl 17	1 ⊢ (𝑀 ∈ Mnd → 𝑀 ∈ Mgm)

Syntax hints:   → wi 4   ∈ wcel 2114  Mgmcmgm 18595  Smgrpcsgrp 18675  Mndcmnd 18691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-nul 5230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6443  df-fv 6495  df-ov 7359  df-sgrp 18676  df-mnd 18692

This theorem is referenced by:  mndcl  18699  mndplusf  18709  ismhm0  18747  mhmismgmhm  18748  mndissubm  18764  grpmgmd  18926  grpissubg  19111  srg1zr  20185  ringmgm  20214  c0mgm  20428  c0snmgmhm  20431  c0snmhm  20432  psdmplcl  22117  psdadd  22118  psdpw  22125  chfacfpmmulgsum2  22818  cayhamlem1  22819  idomrootle  26126  fidomncyc  42968