Theorem wcom2or 409

Description: Th. 4.2 Beran p. 49.

Hypotheses

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

Assertion

Ref	Expression
wcom2or	C (a, (b v c)) = 1

Proof of Theorem wcom2or

Step	Hyp	Ref	Expression
1		wfh.1	. . . . . . . . 9 C (a, b) = 1
2	1	wcomcom 396	. . . . . . . 8 C (b, a) = 1
3	2	wdf-c2 366	. . . . . . 7 (b == ((b ^ a) v (b ^ a_|_))) = 1
4		ancom 68	. . . . . . . . 9 (b ^ a) = (a ^ b)
5		ancom 68	. . . . . . . . 9 (b ^ a_|_) = (a_|_ ^ b)
6	4, 5	2or 67	. . . . . . . 8 ((b ^ a) v (b ^ a_|_)) = ((a ^ b) v (a_|_ ^ b))
7	6	bi1 110	. . . . . . 7 (((b ^ a) v (b ^ a_|_)) == ((a ^ b) v (a_|_ ^ b))) = 1
8	3, 7	wr2 353	. . . . . 6 (b == ((a ^ b) v (a_|_ ^ b))) = 1
9		wfh.2	. . . . . . . . 9 C (a, c) = 1
10	9	wcomcom 396	. . . . . . . 8 C (c, a) = 1
11	10	wdf-c2 366	. . . . . . 7 (c == ((c ^ a) v (c ^ a_|_))) = 1
12		ancom 68	. . . . . . . . 9 (c ^ a) = (a ^ c)
13		ancom 68	. . . . . . . . 9 (c ^ a_|_) = (a_|_ ^ c)
14	12, 13	2or 67	. . . . . . . 8 ((c ^ a) v (c ^ a_|_)) = ((a ^ c) v (a_|_ ^ c))
15	14	bi1 110	. . . . . . 7 (((c ^ a) v (c ^ a_|_)) == ((a ^ c) v (a_|_ ^ c))) = 1
16	11, 15	wr2 353	. . . . . 6 (c == ((a ^ c) v (a_|_ ^ c))) = 1
17	8, 16	w2or 354	. . . . 5 ((b v c) == (((a ^ b) v (a_|_ ^ b)) v ((a ^ c) v (a_|_ ^ c)))) = 1
18		or4 77	. . . . . 6 (((a ^ b) v (a_|_ ^ b)) v ((a ^ c) v (a_|_ ^ c))) = (((a ^ b) v (a ^ c)) v ((a_|_ ^ b) v (a_|_ ^ c)))
19	18	bi1 110	. . . . 5 ((((a ^ b) v (a_|_ ^ b)) v ((a ^ c) v (a_|_ ^ c))) == (((a ^ b) v (a ^ c)) v ((a_|_ ^ b) v (a_|_ ^ c)))) = 1
20	17, 19	wr2 353	. . . 4 ((b v c) == (((a ^ b) v (a ^ c)) v ((a_|_ ^ b) v (a_|_ ^ c)))) = 1
21		ancom 68	. . . . . . . 8 ((b v c) ^ a) = (a ^ (b v c))
22	21	bi1 110	. . . . . . 7 (((b v c) ^ a) == (a ^ (b v c))) = 1
23	1, 9	wfh1 405	. . . . . . 7 ((a ^ (b v c)) == ((a ^ b) v (a ^ c))) = 1
24	22, 23	wr2 353	. . . . . 6 (((b v c) ^ a) == ((a ^ b) v (a ^ c))) = 1
25		ancom 68	. . . . . . . 8 ((b v c) ^ a_|_) = (a_|_ ^ (b v c))
26	25	bi1 110	. . . . . . 7 (((b v c) ^ a_|_) == (a_|_ ^ (b v c))) = 1
27	1	wcomcom3 398	. . . . . . . 8 C (a_|_, b) = 1
28	9	wcomcom3 398	. . . . . . . 8 C (a_|_, c) = 1
29	27, 28	wfh1 405	. . . . . . 7 ((a_|_ ^ (b v c)) == ((a_|_ ^ b) v (a_|_ ^ c))) = 1
30	26, 29	wr2 353	. . . . . 6 (((b v c) ^ a_|_) == ((a_|_ ^ b) v (a_|_ ^ c))) = 1
31	24, 30	w2or 354	. . . . 5 ((((b v c) ^ a) v ((b v c) ^ a_|_)) == (((a ^ b) v (a ^ c)) v ((a_|_ ^ b) v (a_|_ ^ c)))) = 1
32	31	wr1 189	. . . 4 ((((a ^ b) v (a ^ c)) v ((a_|_ ^ b) v (a_|_ ^ c))) == (((b v c) ^ a) v ((b v c) ^ a_|_))) = 1
33	20, 32	wr2 353	. . 3 ((b v c) == (((b v c) ^ a) v ((b v c) ^ a_|_))) = 1
34	33	wdf-c1 365	. 2 C ((b v c), a) = 1
35	34	wcomcom 396	1 C (a, (b v c)) = 1

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

This theorem is referenced by:  wcom2an 410  ska2 414  ska4 415

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