Theorem anass 76

Description: Associative law.

Assertion

Ref	Expression
anass	((a ^ b) ^ c) = (a ^ (b ^ c))

Proof of Theorem anass

Step	Hyp	Ref	Expression
1		ax-a3 32	. . . 4 ((a' v b') v c') = (a' v (b' v c'))
2		df-a 40	. . . . . 6 (a ^ b) = (a' v b')'
3	2	con2 67	. . . . 5 (a ^ b)' = (a' v b')
4	3	ax-r5 38	. . . 4 ((a ^ b)' v c') = ((a' v b') v c')
5		df-a 40	. . . . . 6 (b ^ c) = (b' v c')'
6	5	con2 67	. . . . 5 (b ^ c)' = (b' v c')
7	6	lor 70	. . . 4 (a' v (b ^ c)') = (a' v (b' v c'))
8	1, 4, 7	3tr1 63	. . 3 ((a ^ b)' v c') = (a' v (b ^ c)')
9	8	ax-r4 37	. 2 ((a ^ b)' v c')' = (a' v (b ^ c)')'
10		df-a 40	. 2 ((a ^ b) ^ c) = ((a ^ b)' v c')'
11		df-a 40	. 2 (a ^ (b ^ c)) = (a' v (b ^ c)')'
12	9, 10, 11	3tr1 63	1 ((a ^ b) ^ c) = (a ^ (b ^ c))

Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  an12 81  an32 83  an4 86  mi 125  wanass 204  wwcom3ii 215  wwfh1 216  wwfh2 217  ska6 234  nom11 308  nom14 311  nom15 312  nom21 314  nom24 317  nom25 318  k1-6 353  k1-7 354  2vwomlem 365  wr5-2v 366  wcomlem 382  wcom3ii 419  wfh1 423  wfh2 424  oml5a 450  comcom 453  com3ii 457  fh1 469  fh2 470  oml4 487  gsth 489  i3bi 496  dfi3b 499  i3lem1 504  lem4 511  i3orlem8 559  ud3lem1a 566  ud3lem1b 567  ud3lem2 571  ud3lem3b 573  ud4lem1a 577  ud4lem1b 578  ud4lem2 582  ud4lem3a 583  ud5lem1a 586  ud5lem1b 587  ud5lem1c 588  ud5lem3a 591  ud5lem3b 592  ud5lem3c 593  u2lemaa 601  u3lemaa 602  u4lemaa 603  u5lemaa 604  u1lemab 610  u3lemab 612  u4lemab 613  u5lemab 614  u1lemanb 615  u2lemanb 616  u3lemanb 617  u4lemanb 618  u5lemanb 619  u1lemle2 715  u2lemle2 716  u4lemle2 718  u5lemle2 719  u21lembi 727  u1lem4 757  u4lem5 764  u4lem6 768  u24lem 770  u2lem8 782  u3lem10 785  u3lem11 786  u3lem15 795  3vth1 804  3vth7 810  3vth9 812  3vded21 817  1oa 820  1oaiii 823  2oath1 826  oale 829  mlalem 832  mlaoml 833  bi3 839  bi4 840  mlaconj4 844  mlaconj 845  elimcons2 869  comanblem1 870  comanblem2 871  mh 879  mhcor1 888  oago3.29 889  cancellem 891  govar 896  go2n4 899  go2n6 901  oaidlem2 931  oaidlem2g 932  oa3to4lem1 945  oa3to4lem2 946  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  d4oa 996  oaliii 1001  oalem1 1005  oagen1b 1015  oadist 1019  oadistb 1020  4oagen1b 1042  lem3.3.4 1052  lem3.3.6 1055  lem3.3.7i1e2 1060  lem3.3.7i3e1 1065  lem4.6.2e1 1079

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40

Copyright terms: Public domain