Theorem grpass 18918

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6499  (class class class)co 7367  Basecbs 17179  +_gcplusg 17220  Mndcmnd 18702  Grpcgrp 18909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6455  df-fv 6507  df-ov 7370  df-sgrp 18687  df-mnd 18703  df-grp 18912

This theorem is referenced by:  grpassd  18921  grprcan  18949  grprinv  18966  grpinvid1  18967  grpinvid2  18968  grplcan  18976  grpasscan1  18977  grpasscan2  18978  grpinvadd  18994  grpsubadd  19004  grpaddsubass  19006  grpsubsub4  19009  dfgrp3  19015  grplactcnv  19019  imasgrp  19032  mulgaddcomlem  19073  mulgaddcom  19074  mulgdirlem  19081  issubg2  19117  isnsg3  19135  nmzsubg  19140  ssnmz  19141  eqgcpbl  19157  qusgrp  19161  conjghm  19224  subgga  19275  cntzsubg  19314  sylow1lem2  19574  sylow2blem1  19595  sylow2blem2  19596  sylow2blem3  19597  sylow3lem1  19602  sylow3lem2  19603  lsmass  19644  lsmmod  19650  lsmdisj2  19657  gex2abl  19826  ogrpaddltbi  20114  ogrpaddltrbid  20116  ogrpinvlt  20119  ringcom  20261  lmodass  20871  evpmodpmf1o  21576  ghmcnp  24080  qustgpopn  24085  cnncvsaddassdemo  25130  cyc3genpmlem  33212  archiabllem2c  33256  quslsm  33465  lfladdass  39519  dvhvaddass  41543