Theorem grpass 18960

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095   = wceq 1554   ∈ wcel 2136  ‘cfv 6510  (class class class)co 7385  Basecbs 17221  +_gcplusg 17262  Mndcmnd 18744  Grpcgrp 18951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-nul 5250

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-ov 7388  df-sgrp 18729  df-mnd 18745  df-grp 18954

This theorem is referenced by:  grpassd  18963  grprcan  18991  grprinv  19008  grpinvid1  19009  grpinvid2  19010  grplcan  19018  grpasscan1  19019  grpasscan2  19020  grpinvadd  19036  grpsubadd  19046  grpaddsubass  19048  grpsubsub4  19051  dfgrp3  19057  grplactcnv  19061  imasgrp  19074  mulgaddcomlem  19115  mulgaddcom  19116  mulgdirlem  19123  issubg2  19159  isnsg3  19177  nmzsubg  19182  ssnmz  19183  eqgcpbl  19199  qusgrp  19203  conjghm  19265  subgga  19316  cntzsubg  19355  sylow1lem2  19615  sylow2blem1  19636  sylow2blem2  19637  sylow2blem3  19638  sylow3lem1  19643  sylow3lem2  19644  lsmass  19685  lsmmod  19691  lsmdisj2  19698  gex2abl  19867  ogrpaddltbi  20155  ogrpaddltrbid  20157  ogrpinvlt  20160  ringcom  20302  lmodass  20916  evpmodpmf1o  21621  ghmcnp  24148  qustgpopn  24153  cnncvsaddassdemo  25198  cyc3genpmlem  33285  archiabllem2c  33329  quslsm  33545  lfladdass  39645  dvhvaddass  41669