Theorem an4 86

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

Assertion

Ref	Expression
an4	((a ∩ b) ∩ (c ∩ d)) = ((a ∩ c) ∩ (b ∩ d))

Proof of Theorem an4

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

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:  anandi  114  anandir  115  wwfh2  217  wfh2  424  fh2  470  gsth  489  i3bi  496  ud4lem1a  577  ud5lem1c  588  ud5lem3a  591  ud5lem3c  593  u5lembi  725  u3lem13b  790  3vth7  810  mlalem  832  bi3  839  bi4  840  mlaconj4  844  comanblem1  870  comanblem2  871  mhlem  876  mh  879  marsdenlem3  882  marsdenlem4  883  mhcor1  888  gomaex4  900  gomaex3lem8  921  vneulem16  1146  vneulemexp  1148