Theorem mndmgm 18805

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Mgmcmgm 18702  Smgrpcsgrp 18782  Mndcmnd 18798

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5268

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7415  df-sgrp 18783  df-mnd 18799

This theorem is used by:  mndcl  18806  mndplusf  18816  ismhm0  18854  mhmismgmhm  18855  mndissubm  18871  grpmgmd  19034  grpissubg  19219  srg1zr  20303  ringmgm  20332  c0mgm  20548  c0snmgmhm  20551  c0snmhm  20552  psdmplcl  22336  psdadd  22337  psdpw  22344  chfacfpmmulgsum2  23033  cayhamlem1  23034  idomrootle  26341  fidomncyc  43331