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 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

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

Copyright terms: Public domain