Theorem grpass 19008

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1568   ∈ wcel 2141  ‘cfv 6536  (class class class)co 7410  Basecbs 17268  +_gcplusg 17309  Mndcmnd 18791  Grpcgrp 18999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5268

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-sbc 3744  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413  df-sgrp 18776  df-mnd 18792  df-grp 19002

This theorem is referenced by:  grpassd  19011  grprcan  19039  grprinv  19056  grpinvid1  19057  grpinvid2  19058  grplcan  19066  grpasscan1  19067  grpasscan2  19068  grpinvadd  19083  grpsubadd  19093  grpaddsubass  19095  grpsubsub4  19098  dfgrp3  19104  grplactcnv  19108  imasgrp  19121  mulgaddcomlem  19162  mulgaddcom  19163  mulgdirlem  19170  issubg2  19207  isnsg3  19225  nmzsubg  19230  ssnmz  19231  eqgcpbl  19249  qusgrp  19256  conjghm  19318  subgga  19369  cntzsubg  19408  sylow1lem2  19668  sylow2blem1  19689  sylow2blem2  19690  sylow2blem3  19691  sylow3lem1  19696  sylow3lem2  19697  lsmass  19738  lsmmod  19744  lsmdisj2  19751  gex2abl  19920  ogrpaddltbi  20208  ogrpaddltrbid  20210  ogrpinvlt  20213  ringcom  20362  lmodass  20976  evpmodpmf1o  21725  ghmcnp  24251  qustgpopn  24256  cnncvsaddassdemo  25301  cyc3genpmlem  33437  archiabllem2c  33481  quslsm  33680  lfladdass  39815  dvhvaddass  41839