Theorem grpass 17553

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1596   ∈ wcel 2103  ‘cfv 6001  (class class class)co 6765  Basecbs 15980  +_gcplusg 16064  Mndcmnd 17416  Grpcgrp 17544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-nul 4897

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-iota 5964  df-fv 6009  df-ov 6768  df-sgrp 17406  df-mnd 17417  df-grp 17547

This theorem is referenced by:  grprcan  17577  grprinv  17591  grpinvid1  17592  grpinvid2  17593  grplcan  17599  grpasscan1  17600  grpasscan2  17601  grplmulf1o  17611  grpinvadd  17615  grpsubadd  17625  grpaddsubass  17627  grpsubsub4  17630  dfgrp3  17636  grplactcnv  17640  imasgrp  17653  mulgaddcomlem  17685  mulgaddcom  17686  mulgdirlem  17694  issubg2  17731  isnsg3  17750  nmzsubg  17757  ssnmz  17758  eqger  17766  eqgcpbl  17770  qusgrp  17771  conjghm  17813  conjnmz  17816  subgga  17854  cntzsubg  17890  sylow1lem2  18135  sylow2blem1  18156  sylow2blem2  18157  sylow2blem3  18158  sylow3lem1  18163  sylow3lem2  18164  lsmass  18204  lsmmod  18209  lsmdisj2  18216  gex2abl  18375  ringcom  18700  lmodass  19001  psrgrp  19521  evpmodpmf1o  20065  ghmcnp  22040  qustgpopn  22045  cnncvsaddassdemo  23084  ogrpaddltbi  29949  ogrpaddltrbid  29951  ogrpinvlt  29954  archiabllem2c  29979  lfladdass  34780  dvhvaddass  36805