Theorem mndmgm 18930

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Mgmcmgm 18814  Smgrpcsgrp 18907  Mndcmnd 18923

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-sgrp 18908  df-mnd 18924

This theorem is used by:  mndcl  18931  mndplusf  18942  mndpfo  18947  mndfo  18948  ismhm0  18985  mhmismgmhm  18986  mndissubm  19002  grpmgmd  19172  grpissubg  19357  srg1zr  20441  ringmgm  20471  c0mgm  20689  c0snmgmhm  20692  c0snmhm  20693  psdmplcl  22483  psdadd  22484  psdpw  22491  chfacfpmmulgsum2  23183  cayhamlem1  23184  idomrootle  26491  fidomncyc  43600