Theorem fh4 458

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 441	. . . 4 a' C b'
3		fh.2	. . . . 5 a C c
4	3	comcom4 441	. . . 4 a' C c'
5	2, 4	fh2 456	. . 3 (b' ^ (a' v c')) = ((b' ^ a') v (b' ^ c'))
6		anor2 83	. . . 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 67	. . . . 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 81	. . . 4 ((b' ^ a') v (b' ^ c')) = ((b' ^ a')' ^ (b' ^ c')')'
13		oran 81	. . . . . . 7 (b v a) = (b' ^ a')'
14		oran 81	. . . . . . 7 (b v c) = (b' ^ c')'
15	13, 14	2an 73	. . . . . 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 62	. 2 (b v (a ^ c))' = ((b v a) ^ (b v c))'
20	19	con1 64	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 462  fh4c 464  df2i3 484  i3abs3 510  i3con 537  ud3lem1c 554  ud4lem1c 565  ud4lem1 567  ud5lem1 575  ud5lem3 580  u5lemaa 590  u4lemona 614  u3lemob 618  u3lemonb 623  u1lemc4 687  u2lemc4 688  u3lemc4 689  u4lemc4 690  u5lemc4 691  u4lem1 723  u2lem3 736  u1lem4 743  u4lem5 750  u5lem5 751  u4lem6 754  u5lem6 755  u3lem11 772  orbi 828  e2ast2 880

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 425

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 124  df-le2 125  df-c1 126  df-c2 127

Copyright terms: Public domain