Theorem grpass 18916

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  Mndcmnd 18700  Grpcgrp 18907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-sgrp 18685  df-mnd 18701  df-grp 18910

This theorem is referenced by:  grpassd  18919  grprcan  18947  grprinv  18964  grpinvid1  18965  grpinvid2  18966  grplcan  18974  grpasscan1  18975  grpasscan2  18976  grpinvadd  18992  grpsubadd  19002  grpaddsubass  19004  grpsubsub4  19007  dfgrp3  19013  grplactcnv  19017  imasgrp  19030  mulgaddcomlem  19071  mulgaddcom  19072  mulgdirlem  19079  issubg2  19115  isnsg3  19133  nmzsubg  19138  ssnmz  19139  eqgcpbl  19155  qusgrp  19159  conjghm  19222  subgga  19273  cntzsubg  19312  sylow1lem2  19572  sylow2blem1  19593  sylow2blem2  19594  sylow2blem3  19595  sylow3lem1  19600  sylow3lem2  19601  lsmass  19642  lsmmod  19648  lsmdisj2  19655  gex2abl  19824  ogrpaddltbi  20112  ogrpaddltrbid  20114  ogrpinvlt  20117  ringcom  20259  lmodass  20873  evpmodpmf1o  21578  ghmcnp  24105  qustgpopn  24110  cnncvsaddassdemo  25155  cyc3genpmlem  33239  archiabllem2c  33283  quslsm  33495  lfladdass  39566  dvhvaddass  41590