Theorem grpass 18567

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1541   ∈ wcel 2109  ‘cfv 6430  (class class class)co 7268  Basecbs 16893  +_gcplusg 16943  Mndcmnd 18366  Grpcgrp 18558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-nul 5233

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271  df-sgrp 18356  df-mnd 18367  df-grp 18561

This theorem is referenced by:  grprcan  18594  grprinv  18610  grpinvid1  18611  grpinvid2  18612  grplcan  18618  grpasscan1  18619  grpasscan2  18620  grplmulf1o  18630  grpinvadd  18634  grpsubadd  18644  grpaddsubass  18646  grpsubsub4  18649  dfgrp3  18655  grplactcnv  18659  imasgrp  18672  mulgaddcomlem  18707  mulgaddcom  18708  mulgdirlem  18715  issubg2  18751  isnsg3  18769  nmzsubg  18774  ssnmz  18775  eqger  18787  eqgcpbl  18791  qusgrp  18792  conjghm  18846  conjnmz  18849  subgga  18887  cntzsubg  18924  sylow1lem2  19185  sylow2blem1  19206  sylow2blem2  19207  sylow2blem3  19208  sylow3lem1  19213  sylow3lem2  19214  lsmass  19256  lsmmod  19262  lsmdisj2  19269  gex2abl  19433  ringcom  19799  lmodass  20119  evpmodpmf1o  20782  psrgrp  21148  ghmcnp  23247  qustgpopn  23252  cnncvsaddassdemo  24308  ogrpaddltbi  31323  ogrpaddltrbid  31325  ogrpinvlt  31328  cyc3genpmlem  31397  archiabllem2c  31428  quslsm  31572  lfladdass  37066  dvhvaddass  39090