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 18756	. 2 ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
5	1, 4	sylan 580	1 ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  Mndcmnd 18747  Grpcgrp 18951

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-sgrp 18732  df-mnd 18748  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  19178  nmzsubg  19183  ssnmz  19184  eqgcpbl  19200  qusgrp  19204  conjghm  19267  subgga  19318  cntzsubg  19357  sylow1lem2  19617  sylow2blem1  19638  sylow2blem2  19639  sylow2blem3  19640  sylow3lem1  19645  sylow3lem2  19646  lsmass  19687  lsmmod  19693  lsmdisj2  19700  gex2abl  19869  ringcom  20277  lmodass  20874  evpmodpmf1o  21614  psrgrpOLD  21977  ghmcnp  24123  qustgpopn  24128  cnncvsaddassdemo  25197  ogrpaddltbi  33095  ogrpaddltrbid  33097  ogrpinvlt  33100  cyc3genpmlem  33171  archiabllem2c  33202  quslsm  33433  lfladdass  39074  dvhvaddass  41099