Theorem grpass 18930

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 18928	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	mndass 18726	. 2 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
5	1, 4	sylan 580	1 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ‘cfv 6541  (class class class)co 7413  Basecbs 17230  +_gcplusg 17274  Mndcmnd 18717  Grpcgrp 18921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-nul 5286

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-ov 7416  df-sgrp 18702  df-mnd 18718  df-grp 18924

This theorem is referenced by:  grpassd  18933  grprcan  18961  grprinv  18978  grpinvid1  18979  grpinvid2  18980  grplcan  18988  grpasscan1  18989  grpasscan2  18990  grpinvadd  19006  grpsubadd  19016  grpaddsubass  19018  grpsubsub4  19021  dfgrp3  19027  grplactcnv  19031  imasgrp  19044  mulgaddcomlem  19085  mulgaddcom  19086  mulgdirlem  19093  issubg2  19129  isnsg3  19148  nmzsubg  19153  ssnmz  19154  eqgcpbl  19170  qusgrp  19174  conjghm  19237  subgga  19288  cntzsubg  19327  sylow1lem2  19586  sylow2blem1  19607  sylow2blem2  19608  sylow2blem3  19609  sylow3lem1  19614  sylow3lem2  19615  lsmass  19656  lsmmod  19662  lsmdisj2  19669  gex2abl  19838  ringcom  20246  lmodass  20843  evpmodpmf1o  21569  psrgrpOLD  21932  ghmcnp  24070  qustgpopn  24075  cnncvsaddassdemo  25134  ogrpaddltbi  33039  ogrpaddltrbid  33041  ogrpinvlt  33044  cyc3genpmlem  33115  archiabllem2c  33146  quslsm  33373  lfladdass  39049  dvhvaddass  41074