Theorem mndass 18653

Description: A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.)

Hypotheses

Ref	Expression
mndcl.b	⊢ 𝐵 = (Base‘𝐺)
mndcl.p	⊢ + = (+g‘𝐺)

Assertion

Ref	Expression
mndass	⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Proof of Theorem mndass

Step	Hyp	Ref	Expression
1		mndsgrp 18650	. 2 ⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp)
2		mndcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		mndcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	sgrpass 18635	. 2 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
5	1, 4	sylan 580	1 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6499  (class class class)co 7369  Basecbs 17156  +_gcplusg 17197  Smgrpcsgrp 18628  Mndcmnd 18644

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 5256

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 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-sgrp 18629  df-mnd 18645

This theorem is referenced by:  mnd32g  18656  mnd12g  18657  mnd4g  18658  issubmnd  18671  mndinvmod  18674  prdsmndd  18680  imasmnd  18685  mndvass  18708  mndind  18738  grpass  18857  mhmmnd  18979  cntzsubm  19253  oppgmnd  19269  frgp0  19675  mulgnn0di  19740  gsumval3eu  19819  gsumval3  19822  srgass  20115  srgcom4  20135  ringass  20174  chfacfscmulgsum  22781  chfacfpmmulgsum  22785  mndassd  33008  slmdass  33183  lsmssass  33367  mndmolinv  42077  primrootsunit1  42079  invginvrid  48349  mndtccatid  49570