Theorem fh1 469

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 174	. . 3 ((a ^ b) v (a ^ c)) =< (a ^ (b v c))
2		ancom 74	. . . . . 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 72	. . . . . . . 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 68	. . . . . . . 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 67	. . . . . 6 ((a ^ b) v (a ^ c))' = ((a' v b') ^ (a' v c'))
11	2, 10	2an 79	. . . . 5 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))') = (((b v c) ^ a) ^ ((a' v b') ^ (a' v c')))
12		anass 76	. . . . . . 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 183	. . . . . . . . . . 11 a C b'
15	14	com3ii 457	. . . . . . . . . 10 (a ^ (a' v b')) = (a ^ b')
16		fh.2	. . . . . . . . . . . 12 a C c
17	16	comcom2 183	. . . . . . . . . . 11 a C c'
18	17	com3ii 457	. . . . . . . . . 10 (a ^ (a' v c')) = (a ^ c')
19	15, 18	2an 79	. . . . . . . . 9 ((a ^ (a' v b')) ^ (a ^ (a' v c'))) = ((a ^ b') ^ (a ^ c'))
20		anandi 114	. . . . . . . . 9 (a ^ ((a' v b') ^ (a' v c'))) = ((a ^ (a' v b')) ^ (a ^ (a' v c')))
21		anandi 114	. . . . . . . . 9 (a ^ (b' ^ c')) = ((a ^ b') ^ (a ^ c'))
22	19, 20, 21	3tr1 63	. . . . . . . 8 (a ^ ((a' v b') ^ (a' v c'))) = (a ^ (b' ^ c'))
23	22	lan 77	. . . . . . 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 81	. . . . . 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 87	. . . . . . . . . 10 (b v c) = (b' ^ c')'
29	28	ax-r1 35	. . . . . . . . 9 (b' ^ c')' = (b v c)
30	29	con3 68	. . . . . . . 8 (b' ^ c') = (b v c)'
31	30	lan 77	. . . . . . 7 ((b v c) ^ (b' ^ c')) = ((b v c) ^ (b v c)')
32		dff 101	. . . . . . . 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 77	. . . . 5 (a ^ ((b v c) ^ (b' ^ c'))) = (a ^ 0)
36		an0 108	. . . . 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 452	. 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 471  fh1r 473  com2or 483  nbdi 486  oml4 487  gsth 489  i3bi 496  dfi3b 499  i3lem1 504  lem4 511  i3abs3 524  i3orlem7 558  i3orlem8 559  ud3lem1b 567  ud4lem1a 577  ud4lem1d 580  u5lemaa 604  u3lemc4 703  u4lemle2 718  u5lemle2 719  u5lembi 725  u12lembi 726  u24lem 770  u3lem13a 789  bi1o1a 798  3vded21 817  3vded3 819  comanblem2 871  mhlem1 877  mlaconjolem 885  lem4.6.2e1 1079

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