Theorem fh1 455

Description: Foulis-Holland Theorem.

Hypotheses

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

Assertion

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

Proof of Theorem fh1

Step	Hyp	Ref	Expression
1		ledi 168	. . 3 ((a ^ b) v (a ^ c)) =< (a ^ (b v c))
2		ancom 69	. . . . . 6 (a ^ (b v c)) = ((b v c) ^ a)
3		df-a 40	. . . . . . . . 9 (a ^ b) = (a' v b')'
4		df-a 40	. . . . . . . . 9 (a ^ c) = (a' v c')'
5	3, 4	2or 68	. . . . . . . 8 ((a ^ b) v (a ^ c)) = ((a' v b')' v (a' v c')')
6		df-a 40	. . . . . . . . . 10 ((a' v b') ^ (a' v c')) = ((a' v b')' v (a' v c')')'
7	6	ax-r1 35	. . . . . . . . 9 ((a' v b')' v (a' v c')')' = ((a' v b') ^ (a' v c'))
8	7	con3 66	. . . . . . . 8 ((a' v b')' v (a' v c')') = ((a' v b') ^ (a' v c'))'
9	5, 8	ax-r2 36	. . . . . . 7 ((a ^ b) v (a ^ c)) = ((a' v b') ^ (a' v c'))'
10	9	con2 65	. . . . . 6 ((a ^ b) v (a ^ c))' = ((a' v b') ^ (a' v c'))
11	2, 10	2an 73	. . . . 5 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))') = (((b v c) ^ a) ^ ((a' v b') ^ (a' v c')))
12		anass 70	. . . . . . 7 (((b v c) ^ a) ^ ((a' v b') ^ (a' v c'))) = ((b v c) ^ (a ^ ((a' v b') ^ (a' v c'))))
13		fh.1	. . . . . . . . . . . 12 a C b
14	13	comcom2 177	. . . . . . . . . . 11 a C b'
15	14	com3ii 443	. . . . . . . . . 10 (a ^ (a' v b')) = (a ^ b')
16		fh.2	. . . . . . . . . . . 12 a C c
17	16	comcom2 177	. . . . . . . . . . 11 a C c'
18	17	com3ii 443	. . . . . . . . . 10 (a ^ (a' v c')) = (a ^ c')
19	15, 18	2an 73	. . . . . . . . 9 ((a ^ (a' v b')) ^ (a ^ (a' v c'))) = ((a ^ b') ^ (a ^ c'))
20		anandi 108	. . . . . . . . 9 (a ^ ((a' v b') ^ (a' v c'))) = ((a ^ (a' v b')) ^ (a ^ (a' v c')))
21		anandi 108	. . . . . . . . 9 (a ^ (b' ^ c')) = ((a ^ b') ^ (a ^ c'))
22	19, 20, 21	3tr1 61	. . . . . . . 8 (a ^ ((a' v b') ^ (a' v c'))) = (a ^ (b' ^ c'))
23	22	lan 71	. . . . . . 7 ((b v c) ^ (a ^ ((a' v b') ^ (a' v c')))) = ((b v c) ^ (a ^ (b' ^ c')))
24	12, 23	ax-r2 36	. . . . . 6 (((b v c) ^ a) ^ ((a' v b') ^ (a' v c'))) = ((b v c) ^ (a ^ (b' ^ c')))
25		an12 75	. . . . . 6 ((b v c) ^ (a ^ (b' ^ c'))) = (a ^ ((b v c) ^ (b' ^ c')))
26	24, 25	ax-r2 36	. . . . 5 (((b v c) ^ a) ^ ((a' v b') ^ (a' v c'))) = (a ^ ((b v c) ^ (b' ^ c')))
27	11, 26	ax-r2 36	. . . 4 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))') = (a ^ ((b v c) ^ (b' ^ c')))
28		oran 81	. . . . . . . . . 10 (b v c) = (b' ^ c')'
29	28	ax-r1 35	. . . . . . . . 9 (b' ^ c')' = (b v c)
30	29	con3 66	. . . . . . . 8 (b' ^ c') = (b v c)'
31	30	lan 71	. . . . . . 7 ((b v c) ^ (b' ^ c')) = ((b v c) ^ (b v c)')
32		dff 95	. . . . . . . 8 0 = ((b v c) ^ (b v c)')
33	32	ax-r1 35	. . . . . . 7 ((b v c) ^ (b v c)') = 0
34	31, 33	ax-r2 36	. . . . . 6 ((b v c) ^ (b' ^ c')) = 0
35	34	lan 71	. . . . 5 (a ^ ((b v c) ^ (b' ^ c'))) = (a ^ 0)
36		an0 102	. . . . 5 (a ^ 0) = 0
37	35, 36	ax-r2 36	. . . 4 (a ^ ((b v c) ^ (b' ^ c'))) = 0
38	27, 37	ax-r2 36	. . 3 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))') = 0
39	1, 38	oml3 438	. 2 ((a ^ b) v (a ^ c)) = (a ^ (b v c))
40	39	ax-r1 35	1 (a ^ (b v c)) = ((a ^ b) v (a ^ c))

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

This theorem is referenced by:  fh3 457  fh1r 459  com2or 469  nbdi 472  oml4 473  gsth 475  i3bi 482  dfi3b 485  i3lem1 490  lem4 497  i3abs3 510  i3orlem7 544  i3orlem8 545  ud3lem1b 553  ud4lem1a 563  ud4lem1d 566  u5lemaa 590  u3lemc4 689  u4lemle2 704  u5lemle2 705  u5lembi 711  u12lembi 712  u24lem 756  u3lem13a 775  bi1o1a 784  3vded21 803  3vded3 805  comanblem2 857  mhlem1 863  mlaconjolem 871  lem4.6.2e1 1065

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