Theorem an12 81

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

Assertion

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

Proof of Theorem an12

Step	Hyp	Ref	Expression
1		ancom 74	. . 3 (a ∩ b) = (b ∩ a)
2	1	ran 78	. 2 ((a ∩ b) ∩ c) = ((b ∩ a) ∩ c)
3		anass 76	. 2 ((a ∩ b) ∩ c) = (a ∩ (b ∩ c))
4		anass 76	. 2 ((b ∩ a) ∩ c) = (b ∩ (a ∩ c))
5	2, 3, 4	3tr2 64	1 (a ∩ (b ∩ c)) = (b ∩ (a ∩ c))

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:  an4  86  wwfh1  216  wwfh2  217  wfh1  423  wfh2  424  oml5a  450  fh1  469  fh2  470  i3bi  496  dfi3b  499  ud3lem1b  567  ud4lem1a  577  ud4lem1b  578  ud4lem1d  580  ud5lem1a  586  u4lemle2  718  u12lembi  726  u2lem8  782  1oa  820  mlalem  832  mlaoml  833  bi3  839  bi4  840  mlaconjo  886  cancellem  891  gomaex3lem9  922  testmod  1213