Theorem fh3 471

Description: Foulis-Holland Theorem. (Contributed by NM, 29-Aug-1997.)

Hypotheses

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

Assertion

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

Proof of Theorem fh3

Step	Hyp	Ref	Expression
1		fh.1	. . . . 5 a C b
2	1	comcom4 455	. . . 4 a⊥ C b⊥
3		fh.2	. . . . 5 a C c
4	3	comcom4 455	. . . 4 a⊥ C c⊥
5	2, 4	fh1 469	. . 3 (a⊥ ∩ (b⊥ ∪ c⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ c⊥ ))
6		anor2 89	. . . 4 (a⊥ ∩ (b⊥ ∪ c⊥ )) = (a ∪ (b⊥ ∪ c⊥ )⊥ )⊥
7		df-a 40	. . . . . . 7 (b ∩ c) = (b⊥ ∪ c⊥ )⊥
8	7	ax-r1 35	. . . . . 6 (b⊥ ∪ c⊥ )⊥ = (b ∩ c)
9	8	lor 70	. . . . 5 (a ∪ (b⊥ ∪ c⊥ )⊥ ) = (a ∪ (b ∩ c))
10	9	ax-r4 37	. . . 4 (a ∪ (b⊥ ∪ c⊥ )⊥ )⊥ = (a ∪ (b ∩ c))⊥
11	6, 10	ax-r2 36	. . 3 (a⊥ ∩ (b⊥ ∪ c⊥ )) = (a ∪ (b ∩ c))⊥
12		oran 87	. . . 4 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ c⊥ )) = ((a⊥ ∩ b⊥ )⊥ ∩ (a⊥ ∩ c⊥ )⊥ )⊥
13		oran 87	. . . . . . 7 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
14		oran 87	. . . . . . 7 (a ∪ c) = (a⊥ ∩ c⊥ )⊥
15	13, 14	2an 79	. . . . . 6 ((a ∪ b) ∩ (a ∪ c)) = ((a⊥ ∩ b⊥ )⊥ ∩ (a⊥ ∩ c⊥ )⊥ )
16	15	ax-r1 35	. . . . 5 ((a⊥ ∩ b⊥ )⊥ ∩ (a⊥ ∩ c⊥ )⊥ ) = ((a ∪ b) ∩ (a ∪ c))
17	16	ax-r4 37	. . . 4 ((a⊥ ∩ b⊥ )⊥ ∩ (a⊥ ∩ c⊥ )⊥ )⊥ = ((a ∪ b) ∩ (a ∪ c))⊥
18	12, 17	ax-r2 36	. . 3 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ c⊥ )) = ((a ∪ b) ∩ (a ∪ c))⊥
19	5, 11, 18	3tr2 64	. 2 (a ∪ (b ∩ c))⊥ = ((a ∪ b) ∩ (a ∪ c))⊥
20	19	con1 66	1 (a ∪ (b ∩ c)) = ((a ∪ b) ∩ (a ∪ c))

Syntax hints:   = wb 1   C wc 3  ^⊥ wn 4   ∪ 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:  fh3r  475  i3bi  496  oi3ai3  503  ud1lem2  561  ud1lem3  562  ud2lem3  565  ud3lem1  570  ud4lem1a  577  ud5lem3  594  u4lemob  633  u1lembi  720  u4lem4  759  test  802  3vth5  808  3vth7  810  3vth9  812  1oa  820  2oalem1  825  neg3antlem2  865  comanblem1  870  mhlem  876  gomaex3lem1  914  oau  929  oa23  936  oa3to4lem1  945  oa3to4lem2  946  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa3moa3  1029  lem4.6.2e1  1082  lem4.6.6i1j3  1094  com3iia  1102  lem4.6.7  1103