Theorem anandi 114

Description: Distribution of conjunction over conjunction. (Contributed by NM, 27-Aug-1997.)

Assertion

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

Proof of Theorem anandi

Step	Hyp	Ref	Expression
1		anidm 111	. . . 4 (a ∩ a) = a
2	1	ax-r1 35	. . 3 a = (a ∩ a)
3	2	ran 78	. 2 (a ∩ (b ∩ c)) = ((a ∩ a) ∩ (b ∩ c))
4		an4 86	. 2 ((a ∩ a) ∩ (b ∩ c)) = ((a ∩ b) ∩ (a ∩ c))
5	3, 4	ax-r2 36	1 (a ∩ (b ∩ c)) = ((a ∩ b) ∩ (a ∩ c))

This proof depends on syntax axioms:   = wb 1   ∩ wa 7

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-a 40  df-t 41  df-f 42

This theorem is used by:  wwfh1  216  wdf-c2  384  wfh1  423  fh1  469  i3bi  496  u5lembi  725  u3lem13b  790  3vth9  812  mlaoml  833  comanblem1  870  oa3moa3  1029