Theorem grpass 18114

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ‘cfv 6357  (class class class)co 7158  Basecbs 16485  +_gcplusg 16567  Mndcmnd 17913  Grpcgrp 18105

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 2795  ax-nul 5212

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-sgrp 17903  df-mnd 17914  df-grp 18108

This theorem is referenced by:  grprcan  18139  grprinv  18155  grpinvid1  18156  grpinvid2  18157  grplcan  18163  grpasscan1  18164  grpasscan2  18165  grplmulf1o  18175  grpinvadd  18179  grpsubadd  18189  grpaddsubass  18191  grpsubsub4  18194  dfgrp3  18200  grplactcnv  18204  imasgrp  18217  mulgaddcomlem  18252  mulgaddcom  18253  mulgdirlem  18260  issubg2  18296  isnsg3  18314  nmzsubg  18319  ssnmz  18320  eqger  18332  eqgcpbl  18336  qusgrp  18337  conjghm  18391  conjnmz  18394  subgga  18432  cntzsubg  18469  sylow1lem2  18726  sylow2blem1  18747  sylow2blem2  18748  sylow2blem3  18749  sylow3lem1  18754  sylow3lem2  18755  lsmass  18797  lsmmod  18803  lsmdisj2  18810  gex2abl  18973  ringcom  19331  lmodass  19651  psrgrp  20180  evpmodpmf1o  20742  ghmcnp  22725  qustgpopn  22730  cnncvsaddassdemo  23769  ogrpaddltbi  30721  ogrpaddltrbid  30723  ogrpinvlt  30726  cyc3genpmlem  30795  archiabllem2c  30826  lfladdass  36211  dvhvaddass  38235