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 6498  (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 2708  ax-nul 5241

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  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