Theorem wfh2 406

Description: Weak structural analog of Foulis-Holland Theorem.

Hypotheses

Ref	Expression
wfh.1	C (a, b) = 1
wfh.2	C (a, c) = 1

Assertion

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

Proof of Theorem wfh2

Step	Hyp	Ref	Expression
1		wledi 387	. . 3 (((b ^ a) v (b ^ c)) =<2 (b ^ (a v c))) = 1
2		oran 79	. . . . . . . . . . . 12 ((b ^ a) v (b ^ c)) = ((b ^ a)_|_ ^ (b ^ c)_|_)_|_
3	2	bi1 110	. . . . . . . . . . 11 (((b ^ a) v (b ^ c)) == ((b ^ a)_|_ ^ (b ^ c)_|_)_|_) = 1
4		df-a 39	. . . . . . . . . . . . . . 15 (b ^ a) = (b_|_ v a_|_)_|_
5	4	bi1 110	. . . . . . . . . . . . . 14 ((b ^ a) == (b_|_ v a_|_)_|_) = 1
6	5	wcon2 200	. . . . . . . . . . . . 13 ((b ^ a)_|_ == (b_|_ v a_|_)) = 1
7	6	wran 351	. . . . . . . . . . . 12 (((b ^ a)_|_ ^ (b ^ c)_|_) == ((b_|_ v a_|_) ^ (b ^ c)_|_)) = 1
8	7	wr4 191	. . . . . . . . . . 11 (((b ^ a)_|_ ^ (b ^ c)_|_)_|_ == ((b_|_ v a_|_) ^ (b ^ c)_|_)_|_) = 1
9	3, 8	wr2 353	. . . . . . . . . 10 (((b ^ a) v (b ^ c)) == ((b_|_ v a_|_) ^ (b ^ c)_|_)_|_) = 1
10	9	wcon2 200	. . . . . . . . 9 (((b ^ a) v (b ^ c))_|_ == ((b_|_ v a_|_) ^ (b ^ c)_|_)) = 1
11	10	wlan 352	. . . . . . . 8 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) == ((b ^ (a v c)) ^ ((b_|_ v a_|_) ^ (b ^ c)_|_))) = 1
12		an4 78	. . . . . . . . . 10 ((b ^ (a v c)) ^ ((b_|_ v a_|_) ^ (b ^ c)_|_)) = ((b ^ (b_|_ v a_|_)) ^ ((a v c) ^ (b ^ c)_|_))
13	12	bi1 110	. . . . . . . . 9 (((b ^ (a v c)) ^ ((b_|_ v a_|_) ^ (b ^ c)_|_)) == ((b ^ (b_|_ v a_|_)) ^ ((a v c) ^ (b ^ c)_|_))) = 1
14		wfh.1	. . . . . . . . . . . . . 14 C (a, b) = 1
15	14	wcomcom 396	. . . . . . . . . . . . 13 C (b, a) = 1
16	15	wcomcom2 397	. . . . . . . . . . . 12 C (b, a_|_) = 1
17	16	wcom3ii 401	. . . . . . . . . . 11 ((b ^ (b_|_ v a_|_)) == (b ^ a_|_)) = 1
18		ancom 68	. . . . . . . . . . . 12 (b ^ a_|_) = (a_|_ ^ b)
19	18	bi1 110	. . . . . . . . . . 11 ((b ^ a_|_) == (a_|_ ^ b)) = 1
20	17, 19	wr2 353	. . . . . . . . . 10 ((b ^ (b_|_ v a_|_)) == (a_|_ ^ b)) = 1
21	20	wran 351	. . . . . . . . 9 (((b ^ (b_|_ v a_|_)) ^ ((a v c) ^ (b ^ c)_|_)) == ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_))) = 1
22	13, 21	wr2 353	. . . . . . . 8 (((b ^ (a v c)) ^ ((b_|_ v a_|_) ^ (b ^ c)_|_)) == ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_))) = 1
23	11, 22	wr2 353	. . . . . . 7 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) == ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_))) = 1
24		an4 78	. . . . . . . 8 ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_)) = ((a_|_ ^ (a v c)) ^ (b ^ (b ^ c)_|_))
25	24	bi1 110	. . . . . . 7 (((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_)) == ((a_|_ ^ (a v c)) ^ (b ^ (b ^ c)_|_))) = 1
26	23, 25	wr2 353	. . . . . 6 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) == ((a_|_ ^ (a v c)) ^ (b ^ (b ^ c)_|_))) = 1
27		ax-a1 29	. . . . . . . . . . 11 a = a_|__|_
28	27	bi1 110	. . . . . . . . . 10 (a == a_|__|_) = 1
29	28	wr5-2v 348	. . . . . . . . 9 ((a v c) == (a_|__|_ v c)) = 1
30	29	wlan 352	. . . . . . . 8 ((a_|_ ^ (a v c)) == (a_|_ ^ (a_|__|_ v c))) = 1
31		wfh.2	. . . . . . . . . 10 C (a, c) = 1
32	31	wcomcom3 398	. . . . . . . . 9 C (a_|_, c) = 1
33	32	wcom3ii 401	. . . . . . . 8 ((a_|_ ^ (a_|__|_ v c)) == (a_|_ ^ c)) = 1
34	30, 33	wr2 353	. . . . . . 7 ((a_|_ ^ (a v c)) == (a_|_ ^ c)) = 1
35	34	wran 351	. . . . . 6 (((a_|_ ^ (a v c)) ^ (b ^ (b ^ c)_|_)) == ((a_|_ ^ c) ^ (b ^ (b ^ c)_|_))) = 1
36	26, 35	wr2 353	. . . . 5 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) == ((a_|_ ^ c) ^ (b ^ (b ^ c)_|_))) = 1
37		anass 69	. . . . . 6 ((a_|_ ^ c) ^ (b ^ (b ^ c)_|_)) = (a_|_ ^ (c ^ (b ^ (b ^ c)_|_)))
38	37	bi1 110	. . . . 5 (((a_|_ ^ c) ^ (b ^ (b ^ c)_|_)) == (a_|_ ^ (c ^ (b ^ (b ^ c)_|_)))) = 1
39	36, 38	wr2 353	. . . 4 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) == (a_|_ ^ (c ^ (b ^ (b ^ c)_|_)))) = 1
40		anass 69	. . . . . . . . 9 ((b ^ c) ^ (b ^ c)_|_) = (b ^ (c ^ (b ^ c)_|_))
41	40	bi1 110	. . . . . . . 8 (((b ^ c) ^ (b ^ c)_|_) == (b ^ (c ^ (b ^ c)_|_))) = 1
42	41	wr1 189	. . . . . . 7 ((b ^ (c ^ (b ^ c)_|_)) == ((b ^ c) ^ (b ^ c)_|_)) = 1
43		an12 74	. . . . . . . 8 (c ^ (b ^ (b ^ c)_|_)) = (b ^ (c ^ (b ^ c)_|_))
44	43	bi1 110	. . . . . . 7 ((c ^ (b ^ (b ^ c)_|_)) == (b ^ (c ^ (b ^ c)_|_))) = 1
45		dff 93	. . . . . . . 8 0 = ((b ^ c) ^ (b ^ c)_|_)
46	45	bi1 110	. . . . . . 7 (0 == ((b ^ c) ^ (b ^ c)_|_)) = 1
47	42, 44, 46	w3tr1 356	. . . . . 6 ((c ^ (b ^ (b ^ c)_|_)) == 0) = 1
48	47	wlan 352	. . . . 5 ((a_|_ ^ (c ^ (b ^ (b ^ c)_|_))) == (a_|_ ^ 0)) = 1
49		an0 100	. . . . . 6 (a_|_ ^ 0) = 0
50	49	bi1 110	. . . . 5 ((a_|_ ^ 0) == 0) = 1
51	48, 50	wr2 353	. . . 4 ((a_|_ ^ (c ^ (b ^ (b ^ c)_|_))) == 0) = 1
52	39, 51	wr2 353	. . 3 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) == 0) = 1
53	1, 52	wom5 363	. 2 (((b ^ a) v (b ^ c)) == (b ^ (a v c))) = 1
54	53	wr1 189	1 ((b ^ (a v c)) == ((b ^ a) v (b ^ c))) = 1

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

This theorem is referenced by:  wfh4 408

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-wom 343

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-le 121  df-le1 122  df-le2 123  df-cmtr 126

metamath.org