Theorem grpass 19182

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  +_gcplusg 17457  Mndcmnd 18952  Grpcgrp 19173

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-sgrp 18937  df-mnd 18953  df-grp 19176

This theorem is used by:  grpassd  19185  grprcan  19213  grprinv  19230  grpinvid1  19231  grpinvid2  19232  grplcan  19240  grpasscan1  19241  grpasscan2  19242  grpinvadd  19257  grpsubadd  19267  grpaddsubass  19269  grpsubsub4  19272  dfgrp3  19278  grplactcnv  19282  imasgrp  19295  mulgaddcomlem  19336  mulgaddcom  19337  mulgdirlem  19344  issubg2  19381  isnsg3  19399  nmzsubg  19404  ssnmz  19405  eqgcpbl  19423  qusgrp  19430  conjghm  19492  subgga  19544  cntzsubg  19583  sylow1lem2  19843  sylow2blem1  19864  sylow2blem2  19865  sylow2blem3  19866  sylow3lem1  19871  sylow3lem2  19872  lsmass  19913  lsmmod  19919  lsmdisj2  19926  gex2abl  20095  ogrpaddltbi  20383  ogrpaddltrbid  20385  ogrpinvlt  20388  ringcom  20539  lmodass  21181  evpmodpmf1o  21932  ghmcnp  24464  qustgpopn  24469  cnncvsaddassdemo  25514  cyc3genpmlem  33782  archiabllem2c  33826  quslsm  34026  lfladdass  40322  dvhvaddass  42346