Theorem fh1 451

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 166	. . 3 ((a ^ b) v (a ^ c)) =< (a ^ (b v c))
2		ancom 68	. . . . . 6 (a ^ (b v c)) = ((b v c) ^ a)
3		df-a 39	. . . . . . . . 9 (a ^ b) = (a_|_ v b_|_)_|_
4		df-a 39	. . . . . . . . 9 (a ^ c) = (a_|_ v c_|_)_|_
5	3, 4	2or 67	. . . . . . . 8 ((a ^ b) v (a ^ c)) = ((a_|_ v b_|_)_|_ v (a_|_ v c_|_)_|_)
6		df-a 39	. . . . . . . . . 10 ((a_|_ v b_|_) ^ (a_|_ v c_|_)) = ((a_|_ v b_|_)_|_ v (a_|_ v c_|_)_|_)_|_
7	6	ax-r1 34	. . . . . . . . 9 ((a_|_ v b_|_)_|_ v (a_|_ v c_|_)_|_)_|_ = ((a_|_ v b_|_) ^ (a_|_ v c_|_))
8	7	con3 65	. . . . . . . 8 ((a_|_ v b_|_)_|_ v (a_|_ v c_|_)_|_) = ((a_|_ v b_|_) ^ (a_|_ v c_|_))_|_
9	5, 8	ax-r2 35	. . . . . . 7 ((a ^ b) v (a ^ c)) = ((a_|_ v b_|_) ^ (a_|_ v c_|_))_|_
10	9	con2 64	. . . . . 6 ((a ^ b) v (a ^ c))_|_ = ((a_|_ v b_|_) ^ (a_|_ v c_|_))
11	2, 10	2an 72	. . . . 5 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))_|_) = (((b v c) ^ a) ^ ((a_|_ v b_|_) ^ (a_|_ v c_|_)))
12		anass 69	. . . . . . 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 175	. . . . . . . . . . 11 a C b_|_
15	14	com3ii 439	. . . . . . . . . 10 (a ^ (a_|_ v b_|_)) = (a ^ b_|_)
16		fh.2	. . . . . . . . . . . 12 a C c
17	16	comcom2 175	. . . . . . . . . . 11 a C c_|_
18	17	com3ii 439	. . . . . . . . . 10 (a ^ (a_|_ v c_|_)) = (a ^ c_|_)
19	15, 18	2an 72	. . . . . . . . 9 ((a ^ (a_|_ v b_|_)) ^ (a ^ (a_|_ v c_|_))) = ((a ^ b_|_) ^ (a ^ c_|_))
20		anandi 106	. . . . . . . . 9 (a ^ ((a_|_ v b_|_) ^ (a_|_ v c_|_))) = ((a ^ (a_|_ v b_|_)) ^ (a ^ (a_|_ v c_|_)))
21		anandi 106	. . . . . . . . 9 (a ^ (b_|_ ^ c_|_)) = ((a ^ b_|_) ^ (a ^ c_|_))
22	19, 20, 21	3tr1 60	. . . . . . . 8 (a ^ ((a_|_ v b_|_) ^ (a_|_ v c_|_))) = (a ^ (b_|_ ^ c_|_))
23	22	lan 70	. . . . . . 7 ((b v c) ^ (a ^ ((a_|_ v b_|_) ^ (a_|_ v c_|_)))) = ((b v c) ^ (a ^ (b_|_ ^ c_|_)))
24	12, 23	ax-r2 35	. . . . . 6 (((b v c) ^ a) ^ ((a_|_ v b_|_) ^ (a_|_ v c_|_))) = ((b v c) ^ (a ^ (b_|_ ^ c_|_)))
25		an12 74	. . . . . 6 ((b v c) ^ (a ^ (b_|_ ^ c_|_))) = (a ^ ((b v c) ^ (b_|_ ^ c_|_)))
26	24, 25	ax-r2 35	. . . . 5 (((b v c) ^ a) ^ ((a_|_ v b_|_) ^ (a_|_ v c_|_))) = (a ^ ((b v c) ^ (b_|_ ^ c_|_)))
27	11, 26	ax-r2 35	. . . 4 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))_|_) = (a ^ ((b v c) ^ (b_|_ ^ c_|_)))
28		oran 79	. . . . . . . . . 10 (b v c) = (b_|_ ^ c_|_)_|_
29	28	ax-r1 34	. . . . . . . . 9 (b_|_ ^ c_|_)_|_ = (b v c)
30	29	con3 65	. . . . . . . 8 (b_|_ ^ c_|_) = (b v c)_|_
31	30	lan 70	. . . . . . 7 ((b v c) ^ (b_|_ ^ c_|_)) = ((b v c) ^ (b v c)_|_)
32		dff 93	. . . . . . . 8 0 = ((b v c) ^ (b v c)_|_)
33	32	ax-r1 34	. . . . . . 7 ((b v c) ^ (b v c)_|_) = 0
34	31, 33	ax-r2 35	. . . . . 6 ((b v c) ^ (b_|_ ^ c_|_)) = 0
35	34	lan 70	. . . . 5 (a ^ ((b v c) ^ (b_|_ ^ c_|_))) = (a ^ 0)
36		an0 100	. . . . 5 (a ^ 0) = 0
37	35, 36	ax-r2 35	. . . 4 (a ^ ((b v c) ^ (b_|_ ^ c_|_))) = 0
38	27, 37	ax-r2 35	. . 3 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))_|_) = 0
39	1, 38	oml3 434	. 2 ((a ^ b) v (a ^ c)) = (a ^ (b v c))
40	39	ax-r1 34	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 10

This theorem is referenced by:  fh3 453  fh1r 455  com2or 465  nbdi 468  oml4 469  gsth 471  i3bi 478  dfi3b 481  i3lem1 486  lem4 493  i3abs3 506  i3orlem7 540  i3orlem8 541  ud3lem1b 549  ud4lem1a 559  ud4lem1d 562  u5lemaa 586  u3lemc4 685  u4lemle2 700  u5lemle2 701  u5lembi 707  u12lembi 708  u24lem 752  u3lem13a 771  bi1o1a 780  3vded21 799  3vded3 801  comanblem2 853  mhlem1 859  mlaconjolem 867

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org