Theorem an12 81

Description: Swap conjuncts.

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 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

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