Theorem wfh2 424

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 405	. . 3 (((b ^ a) v (b ^ c)) =<2 (b ^ (a v c))) = 1
2		oran 87	. . . . . . . . . . . 12 ((b ^ a) v (b ^ c)) = ((b ^ a)' ^ (b ^ c)')'
3	2	bi1 118	. . . . . . . . . . 11 (((b ^ a) v (b ^ c)) == ((b ^ a)' ^ (b ^ c)')') = 1
4		df-a 40	. . . . . . . . . . . . . . 15 (b ^ a) = (b' v a')'
5	4	bi1 118	. . . . . . . . . . . . . 14 ((b ^ a) == (b' v a')') = 1
6	5	wcon2 208	. . . . . . . . . . . . 13 ((b ^ a)' == (b' v a')) = 1
7	6	wran 369	. . . . . . . . . . . 12 (((b ^ a)' ^ (b ^ c)') == ((b' v a') ^ (b ^ c)')) = 1
8	7	wr4 199	. . . . . . . . . . 11 (((b ^ a)' ^ (b ^ c)')' == ((b' v a') ^ (b ^ c)')') = 1
9	3, 8	wr2 371	. . . . . . . . . 10 (((b ^ a) v (b ^ c)) == ((b' v a') ^ (b ^ c)')') = 1
10	9	wcon2 208	. . . . . . . . 9 (((b ^ a) v (b ^ c))' == ((b' v a') ^ (b ^ c)')) = 1
11	10	wlan 370	. . . . . . . 8 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == ((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)'))) = 1
12		an4 86	. . . . . . . . . 10 ((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)')) = ((b ^ (b' v a')) ^ ((a v c) ^ (b ^ c)'))
13	12	bi1 118	. . . . . . . . 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 414	. . . . . . . . . . . . 13 C (b, a) = 1
16	15	wcomcom2 415	. . . . . . . . . . . 12 C (b, a') = 1
17	16	wcom3ii 419	. . . . . . . . . . 11 ((b ^ (b' v a')) == (b ^ a')) = 1
18		ancom 74	. . . . . . . . . . . 12 (b ^ a') = (a' ^ b)
19	18	bi1 118	. . . . . . . . . . 11 ((b ^ a') == (a' ^ b)) = 1
20	17, 19	wr2 371	. . . . . . . . . 10 ((b ^ (b' v a')) == (a' ^ b)) = 1
21	20	wran 369	. . . . . . . . 9 (((b ^ (b' v a')) ^ ((a v c) ^ (b ^ c)')) == ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))) = 1
22	13, 21	wr2 371	. . . . . . . 8 (((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)')) == ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))) = 1
23	11, 22	wr2 371	. . . . . . 7 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))) = 1
24		an4 86	. . . . . . . 8 ((a' ^ b) ^ ((a v c) ^ (b ^ c)')) = ((a' ^ (a v c)) ^ (b ^ (b ^ c)'))
25	24	bi1 118	. . . . . . 7 (((a' ^ b) ^ ((a v c) ^ (b ^ c)')) == ((a' ^ (a v c)) ^ (b ^ (b ^ c)'))) = 1
26	23, 25	wr2 371	. . . . . 6 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == ((a' ^ (a v c)) ^ (b ^ (b ^ c)'))) = 1
27		ax-a1 30	. . . . . . . . . . 11 a = a''
28	27	bi1 118	. . . . . . . . . 10 (a == a'') = 1
29	28	wr5-2v 366	. . . . . . . . 9 ((a v c) == (a'' v c)) = 1
30	29	wlan 370	. . . . . . . 8 ((a' ^ (a v c)) == (a' ^ (a'' v c))) = 1
31		wfh.2	. . . . . . . . . 10 C (a, c) = 1
32	31	wcomcom3 416	. . . . . . . . 9 C (a', c) = 1
33	32	wcom3ii 419	. . . . . . . 8 ((a' ^ (a'' v c)) == (a' ^ c)) = 1
34	30, 33	wr2 371	. . . . . . 7 ((a' ^ (a v c)) == (a' ^ c)) = 1
35	34	wran 369	. . . . . 6 (((a' ^ (a v c)) ^ (b ^ (b ^ c)')) == ((a' ^ c) ^ (b ^ (b ^ c)'))) = 1
36	26, 35	wr2 371	. . . . 5 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == ((a' ^ c) ^ (b ^ (b ^ c)'))) = 1
37		anass 76	. . . . . 6 ((a' ^ c) ^ (b ^ (b ^ c)')) = (a' ^ (c ^ (b ^ (b ^ c)')))
38	37	bi1 118	. . . . 5 (((a' ^ c) ^ (b ^ (b ^ c)')) == (a' ^ (c ^ (b ^ (b ^ c)')))) = 1
39	36, 38	wr2 371	. . . 4 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == (a' ^ (c ^ (b ^ (b ^ c)')))) = 1
40		anass 76	. . . . . . . . 9 ((b ^ c) ^ (b ^ c)') = (b ^ (c ^ (b ^ c)'))
41	40	bi1 118	. . . . . . . 8 (((b ^ c) ^ (b ^ c)') == (b ^ (c ^ (b ^ c)'))) = 1
42	41	wr1 197	. . . . . . 7 ((b ^ (c ^ (b ^ c)')) == ((b ^ c) ^ (b ^ c)')) = 1
43		an12 81	. . . . . . . 8 (c ^ (b ^ (b ^ c)')) = (b ^ (c ^ (b ^ c)'))
44	43	bi1 118	. . . . . . 7 ((c ^ (b ^ (b ^ c)')) == (b ^ (c ^ (b ^ c)'))) = 1
45		dff 101	. . . . . . . 8 0 = ((b ^ c) ^ (b ^ c)')
46	45	bi1 118	. . . . . . 7 (0 == ((b ^ c) ^ (b ^ c)')) = 1
47	42, 44, 46	w3tr1 374	. . . . . 6 ((c ^ (b ^ (b ^ c)')) == 0) = 1
48	47	wlan 370	. . . . 5 ((a' ^ (c ^ (b ^ (b ^ c)'))) == (a' ^ 0)) = 1
49		an0 108	. . . . . 6 (a' ^ 0) = 0
50	49	bi1 118	. . . . 5 ((a' ^ 0) == 0) = 1
51	48, 50	wr2 371	. . . 4 ((a' ^ (c ^ (b ^ (b ^ c)'))) == 0) = 1
52	39, 51	wr2 371	. . 3 (((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') == 0) = 1
53	1, 52	wom5 381	. 2 (((b ^ a) v (b ^ c)) == (b ^ (a v c))) = 1
54	53	wr1 197	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 8  0wf 9   C wcmtr 29

This theorem is referenced by:  wfh4 426

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134

Copyright terms: Public domain