Theorem grpass 18881

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  Mndcmnd 18668  Grpcgrp 18872

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-sgrp 18653  df-mnd 18669  df-grp 18875

This theorem is referenced by:  grpassd  18884  grprcan  18912  grprinv  18929  grpinvid1  18930  grpinvid2  18931  grplcan  18939  grpasscan1  18940  grpasscan2  18941  grpinvadd  18957  grpsubadd  18967  grpaddsubass  18969  grpsubsub4  18972  dfgrp3  18978  grplactcnv  18982  imasgrp  18995  mulgaddcomlem  19036  mulgaddcom  19037  mulgdirlem  19044  issubg2  19080  isnsg3  19099  nmzsubg  19104  ssnmz  19105  eqgcpbl  19121  qusgrp  19125  conjghm  19188  subgga  19239  cntzsubg  19278  sylow1lem2  19536  sylow2blem1  19557  sylow2blem2  19558  sylow2blem3  19559  sylow3lem1  19564  sylow3lem2  19565  lsmass  19606  lsmmod  19612  lsmdisj2  19619  gex2abl  19788  ringcom  20196  lmodass  20789  evpmodpmf1o  21512  psrgrpOLD  21873  ghmcnp  24009  qustgpopn  24014  cnncvsaddassdemo  25070  ogrpaddltbi  33039  ogrpaddltrbid  33041  ogrpinvlt  33044  cyc3genpmlem  33115  archiabllem2c  33156  quslsm  33383  lfladdass  39073  dvhvaddass  41098