Theorem grpass 19154

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  (class class class)co 7420  Basecbs 17388  +_gcplusg 17429  Mndcmnd 18924  Grpcgrp 19145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-sgrp 18909  df-mnd 18925  df-grp 19148

This theorem is used by:  grpassd  19157  grprcan  19185  grprinv  19202  grpinvid1  19203  grpinvid2  19204  grplcan  19212  grpasscan1  19213  grpasscan2  19214  grpinvadd  19229  grpsubadd  19239  grpaddsubass  19241  grpsubsub4  19244  dfgrp3  19250  grplactcnv  19254  imasgrp  19267  mulgaddcomlem  19308  mulgaddcom  19309  mulgdirlem  19316  issubg2  19353  isnsg3  19371  nmzsubg  19376  ssnmz  19377  eqgcpbl  19395  qusgrp  19402  conjghm  19464  subgga  19515  cntzsubg  19554  sylow1lem2  19814  sylow2blem1  19835  sylow2blem2  19836  sylow2blem3  19837  sylow3lem1  19842  sylow3lem2  19843  lsmass  19884  lsmmod  19890  lsmdisj2  19897  gex2abl  20066  ogrpaddltbi  20354  ogrpaddltrbid  20356  ogrpinvlt  20359  ringcom  20510  lmodass  21152  evpmodpmf1o  21903  ghmcnp  24435  qustgpopn  24440  cnncvsaddassdemo  25485  cyc3genpmlem  33755  archiabllem2c  33799  quslsm  33999  lfladdass  40206  dvhvaddass  42230