Theorem mndmgm 18615

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

Syntax hints:   → wi 4   ∈ wcel 2109  Mgmcmgm 18512  Smgrpcsgrp 18592  Mndcmnd 18608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-sgrp 18593  df-mnd 18609

This theorem is referenced by:  mndcl  18616  mndplusf  18626  ismhm0  18664  mhmismgmhm  18665  mndissubm  18681  grpmgmd  18840  grpissubg  19025  srg1zr  20100  ringmgm  20129  c0mgm  20344  c0snmgmhm  20347  c0snmhm  20348  psdmplcl  22047  psdadd  22048  psdpw  22055  chfacfpmmulgsum2  22750  cayhamlem1  22751  idomrootle  26076  fidomncyc  42528