Theorem fh2r 474

Description: Foulis-Holland Theorem. (Contributed by NM, 23-Nov-1997.)

Hypotheses

Ref	Expression
fh.1	a C b
fh.2	a C c

Assertion

Ref	Expression
fh2r	((a ∪ c) ∩ b) = ((a ∩ b) ∪ (c ∩ b))

Proof of Theorem fh2r

Step	Hyp	Ref	Expression
1		fh.1	. . 3 a C b
2		fh.2	. . 3 a C c
3	1, 2	fh2 470	. 2 (b ∩ (a ∪ c)) = ((b ∩ a) ∪ (b ∩ c))
4		ancom 74	. 2 ((a ∪ c) ∩ b) = (b ∩ (a ∪ c))
5		ancom 74	. . 3 (a ∩ b) = (b ∩ a)
6		ancom 74	. . 3 (c ∩ b) = (b ∩ c)
7	5, 6	2or 72	. 2 ((a ∩ b) ∪ (c ∩ b)) = ((b ∩ a) ∪ (b ∩ c))
8	3, 4, 7	3tr1 63	1 ((a ∪ c) ∩ b) = ((a ∩ b) ∪ (c ∩ b))

Syntax hints:   = wb 1   C wc 3   ∪ wo 6   ∩ wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  fh2rc  480  ud3lem1a  566  ud3lem2  571  ud3lem3d  575  ud4lem1a  577  ud4lem1b  578  u2lemaa  601  u4lemaa  603  u2lemana  606  u4lemana  608  u1lemab  610  u3lemab  612  u1lemanb  615  u3lemanb  617  u4lemc4  704  u5lemc4  705  u4lem4  759  u24lem  770  bi3  839  bi4  840  marsdenlem1  880  e2astlem1  895  govar  896