Theorem mndmgm 18668

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

Syntax hints:   → wi 4   ∈ wcel 2114  Mgmcmgm 18565  Smgrpcsgrp 18645  Mndcmnd 18661

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 5250

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 2932  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6447  df-fv 6499  df-ov 7361  df-sgrp 18646  df-mnd 18662

This theorem is referenced by:  mndcl  18669  mndplusf  18679  ismhm0  18717  mhmismgmhm  18718  mndissubm  18734  grpmgmd  18893  grpissubg  19078  srg1zr  20152  ringmgm  20181  c0mgm  20397  c0snmgmhm  20400  c0snmhm  20401  psdmplcl  22107  psdadd  22108  psdpw  22115  chfacfpmmulgsum2  22811  cayhamlem1  22812  idomrootle  26136  fidomncyc  42827