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 1540   ∈ wcel 2109  ‘cfv 6536  (class class class)co 7410  Basecbs 17233  +_gcplusg 17276  Mndcmnd 18717  Grpcgrp 18921

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 2708  ax-nul 5281

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 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  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 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  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  19585  sylow2blem1  19606  sylow2blem2  19607  sylow2blem3  19608  sylow3lem1  19613  sylow3lem2  19614  lsmass  19655  lsmmod  19661  lsmdisj2  19668  gex2abl  19837  ringcom  20245  lmodass  20838  evpmodpmf1o  21561  psrgrpOLD  21922  ghmcnp  24058  qustgpopn  24063  cnncvsaddassdemo  25120  ogrpaddltbi  33091  ogrpaddltrbid  33093  ogrpinvlt  33096  cyc3genpmlem  33167  archiabllem2c  33198  quslsm  33425  lfladdass  39096  dvhvaddass  41121