Theorem an32 83

Description: Swap conjuncts. (Contributed by NM, 27-Aug-1997.)

Assertion

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

Proof of Theorem an32

Step	Hyp	Ref	Expression
1		ancom 74	. . 3 (b ∩ c) = (c ∩ b)
2	1	lan 77	. 2 (a ∩ (b ∩ c)) = (a ∩ (c ∩ b))
3		anass 76	. 2 ((a ∩ b) ∩ c) = (a ∩ (b ∩ c))
4		anass 76	. 2 ((a ∩ c) ∩ b) = (a ∩ (c ∩ b))
5	2, 3, 4	3tr1 63	1 ((a ∩ b) ∩ c) = ((a ∩ c) ∩ b)

Syntax hints:   = wb 1   ∩ 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:  lel  151  k1-4  359  wlel  392  gsth  489  i3bi  496  ud2lem2  564  ud3lem1a  566  ud3lem1b  567  ud3lem1d  569  ud3lem2  571  ud3lem3b  573  ud3lem3c  574  ud4lem1a  577  ud4lem1b  578  ud5lem1b  587  ud5lem2  590  ud5lem3a  591  ud5lem3b  592  ud5lem3c  593  u1lemaa  600  u3lemaa  602  u4lemaa  603  u5lemaa  604  u2lemana  606  u3lemana  607  u4lemana  608  u5lemana  609  u3lemab  612  u4lemab  613  u5lemab  614  u3lemanb  617  u2lem1  735  3vth7  810  3vded21  817  mlaoml  833  sadm3  838  bi3  839  bi4  840  mlaconj4  844  comanblem1  870  go2n4  899  gomaex3lem8  921  oa6v4v  933  oalem1  1005  oadistd  1023  4oadist  1044  dp53lemb  1164  dp35lemb  1176  xdp53  1200  xxdp53  1203  xdp43lem  1205  xdp43  1207  3dp43  1208  testmod2  1215  testmod2expanded  1216