Theorem grpass 18112

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  +_gcplusg 16565  Mndcmnd 17911  Grpcgrp 18103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-sgrp 17901  df-mnd 17912  df-grp 18106

This theorem is referenced by:  grprcan  18137  grprinv  18153  grpinvid1  18154  grpinvid2  18155  grplcan  18161  grpasscan1  18162  grpasscan2  18163  grplmulf1o  18173  grpinvadd  18177  grpsubadd  18187  grpaddsubass  18189  grpsubsub4  18192  dfgrp3  18198  grplactcnv  18202  imasgrp  18215  mulgaddcomlem  18250  mulgaddcom  18251  mulgdirlem  18258  issubg2  18294  isnsg3  18312  nmzsubg  18317  ssnmz  18318  eqger  18330  eqgcpbl  18334  qusgrp  18335  conjghm  18389  conjnmz  18392  subgga  18430  cntzsubg  18467  sylow1lem2  18724  sylow2blem1  18745  sylow2blem2  18746  sylow2blem3  18747  sylow3lem1  18752  sylow3lem2  18753  lsmass  18795  lsmmod  18801  lsmdisj2  18808  gex2abl  18971  ringcom  19329  lmodass  19649  psrgrp  20178  evpmodpmf1o  20740  ghmcnp  22723  qustgpopn  22728  cnncvsaddassdemo  23767  ogrpaddltbi  30719  ogrpaddltrbid  30721  ogrpinvlt  30724  cyc3genpmlem  30793  archiabllem2c  30824  lfladdass  36224  dvhvaddass  38248