Theorem grpass 18828

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ‘cfv 6544  (class class class)co 7409  Basecbs 17144  +_gcplusg 17197  Mndcmnd 18625  Grpcgrp 18819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-sgrp 18610  df-mnd 18626  df-grp 18822

This theorem is referenced by:  grpassd  18831  grprcan  18858  grprinv  18875  grpinvid1  18876  grpinvid2  18877  grplcan  18885  grpasscan1  18886  grpasscan2  18887  grplmulf1o  18897  grpinvadd  18901  grpsubadd  18911  grpaddsubass  18913  grpsubsub4  18916  dfgrp3  18922  grplactcnv  18926  imasgrp  18939  mulgaddcomlem  18977  mulgaddcom  18978  mulgdirlem  18985  issubg2  19021  isnsg3  19040  nmzsubg  19045  ssnmz  19046  eqgcpbl  19062  qusgrp  19065  conjghm  19123  conjnmz  19126  subgga  19164  cntzsubg  19203  sylow1lem2  19467  sylow2blem1  19488  sylow2blem2  19489  sylow2blem3  19490  sylow3lem1  19495  sylow3lem2  19496  lsmass  19537  lsmmod  19543  lsmdisj2  19550  gex2abl  19719  ringcom  20097  lmodass  20487  evpmodpmf1o  21149  psrgrpOLD  21518  ghmcnp  23619  qustgpopn  23624  cnncvsaddassdemo  24680  ogrpaddltbi  32267  ogrpaddltrbid  32269  ogrpinvlt  32272  cyc3genpmlem  32341  archiabllem2c  32372  quslsm  32547  lfladdass  37991  dvhvaddass  40016