Theorem grpass 18865

Description: A group operation is associative. (Contributed by NM, 14-Aug-2011.)

Hypotheses

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

Assertion

Ref	Expression
grpass	⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Proof of Theorem grpass

Step	Hyp	Ref	Expression
1		grpmnd 18863	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	mndass 18661	. 2 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
5	1, 4	sylan 580	1 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6489  (class class class)co 7355  Basecbs 17130  +_gcplusg 17171  Mndcmnd 18652  Grpcgrp 18856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-sgrp 18637  df-mnd 18653  df-grp 18859

This theorem is referenced by:  grpassd  18868  grprcan  18896  grprinv  18913  grpinvid1  18914  grpinvid2  18915  grplcan  18923  grpasscan1  18924  grpasscan2  18925  grpinvadd  18941  grpsubadd  18951  grpaddsubass  18953  grpsubsub4  18956  dfgrp3  18962  grplactcnv  18966  imasgrp  18979  mulgaddcomlem  19020  mulgaddcom  19021  mulgdirlem  19028  issubg2  19064  isnsg3  19082  nmzsubg  19087  ssnmz  19088  eqgcpbl  19104  qusgrp  19108  conjghm  19171  subgga  19222  cntzsubg  19261  sylow1lem2  19521  sylow2blem1  19542  sylow2blem2  19543  sylow2blem3  19544  sylow3lem1  19549  sylow3lem2  19550  lsmass  19591  lsmmod  19597  lsmdisj2  19604  gex2abl  19773  ogrpaddltbi  20061  ogrpaddltrbid  20063  ogrpinvlt  20066  ringcom  20208  lmodass  20819  evpmodpmf1o  21543  psrgrpOLD  21904  ghmcnp  24040  qustgpopn  24045  cnncvsaddassdemo  25100  cyc3genpmlem  33131  archiabllem2c  33175  quslsm  33381  lfladdass  39182  dvhvaddass  41206