Theorem an12 74

Description: Swap conjuncts.

Assertion

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

Proof of Theorem an12

Step	Hyp	Ref	Expression
1		ancom 68	. . 3 (a ∩ b) = (b ∩ a)
2	1	ran 71	. 2 ((a ∩ b) ∩ c) = ((b ∩ a) ∩ c)
3		anass 69	. 2 ((a ∩ b) ∩ c) = (a ∩ (b ∩ c))
4		anass 69	. 2 ((b ∩ a) ∩ c) = (b ∩ (a ∩ c))
5	2, 3, 4	3tr2 61	1 (a ∩ (b ∩ c)) = (b ∩ (a ∩ c))

Syntax hints:   = wb 1   ∩ wa 7

This theorem is referenced by:  an4 78  wwfh1 208  wwfh2 209  wfh1 405  wfh2 406  oml5a 432  fh1 451  fh2 452  i3bi 478  dfi3b 481  ud3lem1b 549  ud4lem1a 559  ud4lem1b 560  ud4lem1d 562  ud5lem1a 568  u4lemle2 700  u12lembi 708  u2lem8 764  1oa 802  mlalem 814  mlaoml 815  bi3 821  bi4 822  mlaconjo 868  cancellem 873  gomaex3lem9 902

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