Theorem grpass 19070

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 19068	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpcl.p	. . 3 ⊢ + = (+g‘𝐺)
4	2, 3	mndass 18849	. 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 6537  (class class class)co 7416  Basecbs 17305  +_gcplusg 17346  Mndcmnd 18840  Grpcgrp 19061

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 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419  df-sgrp 18825  df-mnd 18841  df-grp 19064

This theorem is used by:  grpassd  19073  grprcan  19101  grprinv  19118  grpinvid1  19119  grpinvid2  19120  grplcan  19128  grpasscan1  19129  grpasscan2  19130  grpinvadd  19145  grpsubadd  19155  grpaddsubass  19157  grpsubsub4  19160  dfgrp3  19166  grplactcnv  19170  imasgrp  19183  mulgaddcomlem  19224  mulgaddcom  19225  mulgdirlem  19232  issubg2  19269  isnsg3  19287  nmzsubg  19292  ssnmz  19293  eqgcpbl  19311  qusgrp  19318  conjghm  19380  subgga  19431  cntzsubg  19470  sylow1lem2  19730  sylow2blem1  19751  sylow2blem2  19752  sylow2blem3  19753  sylow3lem1  19758  sylow3lem2  19759  lsmass  19800  lsmmod  19806  lsmdisj2  19813  gex2abl  19982  ogrpaddltbi  20270  ogrpaddltrbid  20272  ogrpinvlt  20275  ringcom  20425  lmodass  21064  evpmodpmf1o  21813  ghmcnp  24345  qustgpopn  24350  cnncvsaddassdemo  25395  cyc3genpmlem  33593  archiabllem2c  33637  quslsm  33836  lfladdass  39948  dvhvaddass  41972