Theorem fh4 472

Description: Foulis-Holland Theorem.

Hypotheses

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

Assertion

Ref	Expression
fh4	(b v (a ^ c)) = ((b v a) ^ (b v c))

Proof of Theorem fh4

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	fh2 470	. . 3 (b' ^ (a' v c')) = ((b' ^ a') v (b' ^ c'))
6		anor2 89	. . . 4 (b' ^ (a' v c')) = (b v (a' v c')')'
7		df-a 40	. . . . . . 7 (a ^ c) = (a' v c')'
8	7	ax-r1 35	. . . . . 6 (a' v c')' = (a ^ c)
9	8	lor 70	. . . . 5 (b v (a' v c')') = (b v (a ^ c))
10	9	ax-r4 37	. . . 4 (b v (a' v c')')' = (b v (a ^ c))'
11	6, 10	ax-r2 36	. . 3 (b' ^ (a' v c')) = (b v (a ^ c))'
12		oran 87	. . . 4 ((b' ^ a') v (b' ^ c')) = ((b' ^ a')' ^ (b' ^ c')')'
13		oran 87	. . . . . . 7 (b v a) = (b' ^ a')'
14		oran 87	. . . . . . 7 (b v c) = (b' ^ c')'
15	13, 14	2an 79	. . . . . 6 ((b v a) ^ (b v c)) = ((b' ^ a')' ^ (b' ^ c')')
16	15	ax-r1 35	. . . . 5 ((b' ^ a')' ^ (b' ^ c')') = ((b v a) ^ (b v c))
17	16	ax-r4 37	. . . 4 ((b' ^ a')' ^ (b' ^ c')')' = ((b v a) ^ (b v c))'
18	12, 17	ax-r2 36	. . 3 ((b' ^ a') v (b' ^ c')) = ((b v a) ^ (b v c))'
19	5, 11, 18	3tr2 64	. 2 (b v (a ^ c))' = ((b v a) ^ (b v c))'
20	19	con1 66	1 (b v (a ^ c)) = ((b v a) ^ (b v c))

Syntax hints:   = wb 1   C wc 3  'wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  fh4r 476  fh4c 478  df2i3 498  i3abs3 524  i3con 551  ud3lem1c 568  ud4lem1c 579  ud4lem1 581  ud5lem1 589  ud5lem3 594  u5lemaa 604  u4lemona 628  u3lemob 632  u3lemonb 637  u1lemc4 701  u2lemc4 702  u3lemc4 703  u4lemc4 704  u5lemc4 705  u4lem1 737  u2lem3 750  u1lem4 757  u4lem5 764  u5lem5 765  u4lem6 768  u5lem6 769  u3lem11 786  orbi 842  e2ast2 894

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