Theorem fh1r 473

Description: Foulis-Holland Theorem.

Hypotheses

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

Assertion

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

Proof of Theorem fh1r

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

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:  fh1rc  479  gsth  489  dfi3b  499  ud3lem1b  567  ud3lem1d  569  ud3lem3d  575  ud5lem1a  586  ud5lem3a  591  u1lemaa  600  u3lemaa  602  u4lemaa  603  u5lemaa  604  u3lemana  607  u4lemana  608  u5lemana  609  u3lemab  612  u4lemab  613  u5lemab  614  u2lemanb  616  u4lemanb  618  u5lemanb  619  u4lem4  759  u4lem5  764  u5lem5  765  u5lem6  769  u1lem8  776  u3lem15  795  bi1o1a  798  3vded21  817  1oa  820  neg3antlem2  865  mhlem  876  mhlem1  877  marsdenlem3  882  marsdenlem4  883