Theorem anass 76

Description: Associative law. (Contributed by NM, 12-Aug-1997.)

Assertion

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

Proof of Theorem anass

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

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

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

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  oa3moa3  1029  4oagen1b  1043  lem3.3.4  1053  lem3.3.6  1056  lem3.3.7i1e2  1061  lem3.3.7i3e1  1066  lem4.6.2e1  1082  vneulem2  1132  vneulemexp  1148  modexp  1152  dp53lemb  1164  dp53lemf  1168  dp35leme  1173  dp35lemb  1176  dp41lemb  1183  dp41lemc  1185  dp41leme  1187  xdp41  1198  xdp53  1200  xxdp41  1201  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod2  1215  testmod2expanded  1216