Theorem wwfh2 209

Description: Foulis-Holland Theorem (weak).

Hypotheses

Ref	Expression
wwfh2.1	a C b
wwfh2.2	c_|_ C a

Assertion

Ref	Expression
wwfh2	((b ^ (a v c)) == ((b ^ a) v (b ^ c))) = 1

Proof of Theorem wwfh2

Step	Hyp	Ref	Expression
1		bicom 88	. 2 ((b ^ (a v c)) == ((b ^ a) v (b ^ c))) = (((b ^ a) v (b ^ c)) == (b ^ (a v c)))
2		ledi 166	. . 3 ((b ^ a) v (b ^ c)) =< (b ^ (a v c))
3		oran 79	. . . . . . . . . . 11 ((b ^ a) v (b ^ c)) = ((b ^ a)_|_ ^ (b ^ c)_|_)_|_
4		df-a 39	. . . . . . . . . . . . . 14 (b ^ a) = (b_|_ v a_|_)_|_
5	4	con2 64	. . . . . . . . . . . . 13 (b ^ a)_|_ = (b_|_ v a_|_)
6	5	ran 71	. . . . . . . . . . . 12 ((b ^ a)_|_ ^ (b ^ c)_|_) = ((b_|_ v a_|_) ^ (b ^ c)_|_)
7	6	ax-r4 36	. . . . . . . . . . 11 ((b ^ a)_|_ ^ (b ^ c)_|_)_|_ = ((b_|_ v a_|_) ^ (b ^ c)_|_)_|_
8	3, 7	ax-r2 35	. . . . . . . . . 10 ((b ^ a) v (b ^ c)) = ((b_|_ v a_|_) ^ (b ^ c)_|_)_|_
9	8	con2 64	. . . . . . . . 9 ((b ^ a) v (b ^ c))_|_ = ((b_|_ v a_|_) ^ (b ^ c)_|_)
10	9	lan 70	. . . . . . . 8 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = ((b ^ (a v c)) ^ ((b_|_ v a_|_) ^ (b ^ c)_|_))
11		an4 78	. . . . . . . . 9 ((b ^ (a v c)) ^ ((b_|_ v a_|_) ^ (b ^ c)_|_)) = ((b ^ (b_|_ v a_|_)) ^ ((a v c) ^ (b ^ c)_|_))
12		ax-a1 29	. . . . . . . . . . . . . 14 a = a_|__|_
13	12	ax-r1 34	. . . . . . . . . . . . 13 a_|__|_ = a
14		wwfh2.1	. . . . . . . . . . . . 13 a C b
15	13, 14	bctr 173	. . . . . . . . . . . 12 a_|__|_ C b
16	15	wwcom3ii 207	. . . . . . . . . . 11 (b ^ (b_|_ v a_|_)) = (b ^ a_|_)
17		ancom 68	. . . . . . . . . . 11 (b ^ a_|_) = (a_|_ ^ b)
18	16, 17	ax-r2 35	. . . . . . . . . 10 (b ^ (b_|_ v a_|_)) = (a_|_ ^ b)
19	18	ran 71	. . . . . . . . 9 ((b ^ (b_|_ v a_|_)) ^ ((a v c) ^ (b ^ c)_|_)) = ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_))
20	11, 19	ax-r2 35	. . . . . . . 8 ((b ^ (a v c)) ^ ((b_|_ v a_|_) ^ (b ^ c)_|_)) = ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_))
21	10, 20	ax-r2 35	. . . . . . 7 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_))
22		an4 78	. . . . . . 7 ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_)) = ((a_|_ ^ (a v c)) ^ (b ^ (b ^ c)_|_))
23	21, 22	ax-r2 35	. . . . . 6 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = ((a_|_ ^ (a v c)) ^ (b ^ (b ^ c)_|_))
24	12	ax-r5 37	. . . . . . . . 9 (a v c) = (a_|__|_ v c)
25	24	lan 70	. . . . . . . 8 (a_|_ ^ (a v c)) = (a_|_ ^ (a_|__|_ v c))
26		wwfh2.2	. . . . . . . . . 10 c_|_ C a
27	26	comcom2 175	. . . . . . . . 9 c_|_ C a_|_
28	27	wwcom3ii 207	. . . . . . . 8 (a_|_ ^ (a_|__|_ v c)) = (a_|_ ^ c)
29	25, 28	ax-r2 35	. . . . . . 7 (a_|_ ^ (a v c)) = (a_|_ ^ c)
30	29	ran 71	. . . . . 6 ((a_|_ ^ (a v c)) ^ (b ^ (b ^ c)_|_)) = ((a_|_ ^ c) ^ (b ^ (b ^ c)_|_))
31	23, 30	ax-r2 35	. . . . 5 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = ((a_|_ ^ c) ^ (b ^ (b ^ c)_|_))
32		anass 69	. . . . 5 ((a_|_ ^ c) ^ (b ^ (b ^ c)_|_)) = (a_|_ ^ (c ^ (b ^ (b ^ c)_|_)))
33	31, 32	ax-r2 35	. . . 4 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = (a_|_ ^ (c ^ (b ^ (b ^ c)_|_)))
34		anass 69	. . . . . . . 8 ((b ^ c) ^ (b ^ c)_|_) = (b ^ (c ^ (b ^ c)_|_))
35	34	ax-r1 34	. . . . . . 7 (b ^ (c ^ (b ^ c)_|_)) = ((b ^ c) ^ (b ^ c)_|_)
36		an12 74	. . . . . . 7 (c ^ (b ^ (b ^ c)_|_)) = (b ^ (c ^ (b ^ c)_|_))
37		dff 93	. . . . . . 7 0 = ((b ^ c) ^ (b ^ c)_|_)
38	35, 36, 37	3tr1 60	. . . . . 6 (c ^ (b ^ (b ^ c)_|_)) = 0
39	38	lan 70	. . . . 5 (a_|_ ^ (c ^ (b ^ (b ^ c)_|_))) = (a_|_ ^ 0)
40		an0 100	. . . . 5 (a_|_ ^ 0) = 0
41	39, 40	ax-r2 35	. . . 4 (a_|_ ^ (c ^ (b ^ (b ^ c)_|_))) = 0
42	33, 41	ax-r2 35	. . 3 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = 0
43	2, 42	wwoml3 205	. 2 (((b ^ a) v (b ^ c)) == (b ^ (a v c))) = 1
44	1, 43	ax-r2 35	1 ((b ^ (a v c)) == ((b ^ a) v (b ^ c))) = 1

Syntax hints:   = wb 1   C wc 3  _|_wn 4   == tb 5   v wo 6   ^ wa 7  1wt 9  0wf 10

This theorem is referenced by:  wwfh4 211

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

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