Theorem grpass 18839

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  +_gcplusg 17179  Mndcmnd 18626  Grpcgrp 18830

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 2701  ax-nul 5248

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-sgrp 18611  df-mnd 18627  df-grp 18833

This theorem is referenced by:  grpassd  18842  grprcan  18870  grprinv  18887  grpinvid1  18888  grpinvid2  18889  grplcan  18897  grpasscan1  18898  grpasscan2  18899  grpinvadd  18915  grpsubadd  18925  grpaddsubass  18927  grpsubsub4  18930  dfgrp3  18936  grplactcnv  18940  imasgrp  18953  mulgaddcomlem  18994  mulgaddcom  18995  mulgdirlem  19002  issubg2  19038  isnsg3  19057  nmzsubg  19062  ssnmz  19063  eqgcpbl  19079  qusgrp  19083  conjghm  19146  subgga  19197  cntzsubg  19236  sylow1lem2  19496  sylow2blem1  19517  sylow2blem2  19518  sylow2blem3  19519  sylow3lem1  19524  sylow3lem2  19525  lsmass  19566  lsmmod  19572  lsmdisj2  19579  gex2abl  19748  ogrpaddltbi  20036  ogrpaddltrbid  20038  ogrpinvlt  20041  ringcom  20183  lmodass  20797  evpmodpmf1o  21521  psrgrpOLD  21882  ghmcnp  24018  qustgpopn  24023  cnncvsaddassdemo  25079  cyc3genpmlem  33106  archiabllem2c  33147  quslsm  33352  lfladdass  39051  dvhvaddass  41076