Theorem grpass 19115

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6527  (class class class)co 7408  Basecbs 17349  +_gcplusg 17390  Mndcmnd 18885  Grpcgrp 19106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411  df-sgrp 18870  df-mnd 18886  df-grp 19109

This theorem is used by:  grpassd  19118  grprcan  19146  grprinv  19163  grpinvid1  19164  grpinvid2  19165  grplcan  19173  grpasscan1  19174  grpasscan2  19175  grpinvadd  19190  grpsubadd  19200  grpaddsubass  19202  grpsubsub4  19205  dfgrp3  19211  grplactcnv  19215  imasgrp  19228  mulgaddcomlem  19269  mulgaddcom  19270  mulgdirlem  19277  issubg2  19314  isnsg3  19332  nmzsubg  19337  ssnmz  19338  eqgcpbl  19356  qusgrp  19363  conjghm  19425  subgga  19476  cntzsubg  19515  sylow1lem2  19775  sylow2blem1  19796  sylow2blem2  19797  sylow2blem3  19798  sylow3lem1  19803  sylow3lem2  19804  lsmass  19845  lsmmod  19851  lsmdisj2  19858  gex2abl  20027  ogrpaddltbi  20315  ogrpaddltrbid  20317  ogrpinvlt  20320  ringcom  20471  lmodass  21113  evpmodpmf1o  21864  ghmcnp  24396  qustgpopn  24401  cnncvsaddassdemo  25446  cyc3genpmlem  33646  archiabllem2c  33690  quslsm  33890  lfladdass  40050  dvhvaddass  42074