Theorem an32 76

Description: Swap conjuncts.

Assertion

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

Proof of Theorem an32

Step	Hyp	Ref	Expression
1		ancom 68	. . 3 (b ∩ c) = (c ∩ b)
2	1	lan 70	. 2 (a ∩ (b ∩ c)) = (a ∩ (c ∩ b))
3		anass 69	. 2 ((a ∩ b) ∩ c) = (a ∩ (b ∩ c))
4		anass 69	. 2 ((a ∩ c) ∩ b) = (a ∩ (c ∩ b))
5	2, 3, 4	3tr1 60	1 ((a ∩ b) ∩ c) = ((a ∩ c) ∩ b)

Syntax hints:   = wb 1   ∩ wa 7

This theorem is referenced by:  lel 143  wlel 374  gsth 471  i3bi 478  ud2lem2 546  ud3lem1a 548  ud3lem1b 549  ud3lem1d 551  ud3lem2 553  ud3lem3b 555  ud3lem3c 556  ud4lem1a 559  ud4lem1b 560  ud5lem1b 569  ud5lem2 572  ud5lem3a 573  ud5lem3b 574  ud5lem3c 575  u1lemaa 582  u3lemaa 584  u4lemaa 585  u5lemaa 586  u2lemana 588  u3lemana 589  u4lemana 590  u5lemana 591  u3lemab 594  u4lemab 595  u5lemab 596  u3lemanb 599  u2lem1 717  3vth7 792  3vded21 799  mlaoml 815  sadm3 820  bi3 821  bi4 822  mlaconj4 826  comanblem1 852  go2n4 879  gomaex3lem8 901  oa6v4v 913  oalem1 985  oadistd 1003  4oadist 1023

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