Theorem anass 69

Description: Associative law.

Assertion

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

Proof of Theorem anass

Step	Hyp	Ref	Expression
1		ax-a3 31	. . . 4 ((a⊥ ∪ b⊥ ) ∪ c⊥ ) = (a⊥ ∪ (b⊥ ∪ c⊥ ))
2		df-a 39	. . . . . 6 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
3	2	con2 64	. . . . 5 (a ∩ b)⊥ = (a⊥ ∪ b⊥ )
4	3	ax-r5 37	. . . 4 ((a ∩ b)⊥ ∪ c⊥ ) = ((a⊥ ∪ b⊥ ) ∪ c⊥ )
5		df-a 39	. . . . . 6 (b ∩ c) = (b⊥ ∪ c⊥ )⊥
6	5	con2 64	. . . . 5 (b ∩ c)⊥ = (b⊥ ∪ c⊥ )
7	6	lor 66	. . . 4 (a⊥ ∪ (b ∩ c)⊥ ) = (a⊥ ∪ (b⊥ ∪ c⊥ ))
8	1, 4, 7	3tr1 60	. . 3 ((a ∩ b)⊥ ∪ c⊥ ) = (a⊥ ∪ (b ∩ c)⊥ )
9	8	ax-r4 36	. 2 ((a ∩ b)⊥ ∪ c⊥ )⊥ = (a⊥ ∪ (b ∩ c)⊥ )⊥
10		df-a 39	. 2 ((a ∩ b) ∩ c) = ((a ∩ b)⊥ ∪ c⊥ )⊥
11		df-a 39	. 2 (a ∩ (b ∩ c)) = (a⊥ ∪ (b ∩ c)⊥ )⊥
12	9, 10, 11	3tr1 60	1 ((a ∩ b) ∩ c) = (a ∩ (b ∩ c))

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This theorem is referenced by:  an12 74  an32 76  an4 78  mi 117  wanass 196  wwcom3ii 207  wwfh1 208  wwfh2 209  ska6 226  nom11 300  nom14 303  nom15 304  nom21 306  nom24 309  nom25 310  2vwomlem 347  wr5-2v 348  wcomlem 364  wcom3ii 401  wfh1 405  wfh2 406  oml5a 432  comcom 435  com3ii 439  fh1 451  fh2 452  oml4 469  gsth 471  i3bi 478  dfi3b 481  i3lem1 486  lem4 493  i3orlem8 541  ud3lem1a 548  ud3lem1b 549  ud3lem2 553  ud3lem3b 555  ud4lem1a 559  ud4lem1b 560  ud4lem2 564  ud4lem3a 565  ud5lem1a 568  ud5lem1b 569  ud5lem1c 570  ud5lem3a 573  ud5lem3b 574  ud5lem3c 575  u2lemaa 583  u3lemaa 584  u4lemaa 585  u5lemaa 586  u1lemab 592  u3lemab 594  u4lemab 595  u5lemab 596  u1lemanb 597  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u1lemle2 697  u2lemle2 698  u4lemle2 700  u5lemle2 701  u21lembi 709  u1lem4 739  u4lem5 746  u4lem6 750  u24lem 752  u2lem8 764  u3lem10 767  u3lem11 768  u3lem15 777  3vth1 786  3vth7 792  3vth9 794  3vded21 799  1oa 802  1oaiii 805  2oath1 808  oale 811  mlalem 814  mlaoml 815  bi3 821  bi4 822  mlaconj4 826  mlaconj 827  elimcons2 851  comanblem1 852  comanblem2 853  mh 861  mhcor1 870  oago3.29 871  cancellem 873  govar 876  go2n4 879  go2n6 881  oaidlem2 911  oaidlem2g 912  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  d4oa 976  oaliii 981  oalem1 985  oagen1b 995  oadist 999  oadistb 1000  4oagen1b 1022

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

This theorem depends on definitions:  df-a 39

metamath.org