Theorem wcom2or 427

Description: Thm. 4.2 Beran p. 49. (Contributed by NM, 10-Nov-1998.)

Hypotheses

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

Assertion

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

Proof of Theorem wcom2or

Step	Hyp	Ref	Expression
1		wfh.1	. . . . . . . . 9 C (a, b) = 1
2	1	wcomcom 414	. . . . . . . 8 C (b, a) = 1
3	2	wdf-c2 384	. . . . . . 7 (b ≡ ((b ∩ a) ∪ (b ∩ a⊥ ))) = 1
4		ancom 74	. . . . . . . . 9 (b ∩ a) = (a ∩ b)
5		ancom 74	. . . . . . . . 9 (b ∩ a⊥ ) = (a⊥ ∩ b)
6	4, 5	2or 72	. . . . . . . 8 ((b ∩ a) ∪ (b ∩ a⊥ )) = ((a ∩ b) ∪ (a⊥ ∩ b))
7	6	bi1 118	. . . . . . 7 (((b ∩ a) ∪ (b ∩ a⊥ )) ≡ ((a ∩ b) ∪ (a⊥ ∩ b))) = 1
8	3, 7	wr2 371	. . . . . 6 (b ≡ ((a ∩ b) ∪ (a⊥ ∩ b))) = 1
9		wfh.2	. . . . . . . . 9 C (a, c) = 1
10	9	wcomcom 414	. . . . . . . 8 C (c, a) = 1
11	10	wdf-c2 384	. . . . . . 7 (c ≡ ((c ∩ a) ∪ (c ∩ a⊥ ))) = 1
12		ancom 74	. . . . . . . . 9 (c ∩ a) = (a ∩ c)
13		ancom 74	. . . . . . . . 9 (c ∩ a⊥ ) = (a⊥ ∩ c)
14	12, 13	2or 72	. . . . . . . 8 ((c ∩ a) ∪ (c ∩ a⊥ )) = ((a ∩ c) ∪ (a⊥ ∩ c))
15	14	bi1 118	. . . . . . 7 (((c ∩ a) ∪ (c ∩ a⊥ )) ≡ ((a ∩ c) ∪ (a⊥ ∩ c))) = 1
16	11, 15	wr2 371	. . . . . 6 (c ≡ ((a ∩ c) ∪ (a⊥ ∩ c))) = 1
17	8, 16	w2or 372	. . . . 5 ((b ∪ c) ≡ (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ c) ∪ (a⊥ ∩ c)))) = 1
18		or4 84	. . . . . 6 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ c) ∪ (a⊥ ∩ c))) = (((a ∩ b) ∪ (a ∩ c)) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ c)))
19	18	bi1 118	. . . . 5 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a ∩ c) ∪ (a⊥ ∩ c))) ≡ (((a ∩ b) ∪ (a ∩ c)) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ c)))) = 1
20	17, 19	wr2 371	. . . 4 ((b ∪ c) ≡ (((a ∩ b) ∪ (a ∩ c)) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ c)))) = 1
21		ancom 74	. . . . . . . 8 ((b ∪ c) ∩ a) = (a ∩ (b ∪ c))
22	21	bi1 118	. . . . . . 7 (((b ∪ c) ∩ a) ≡ (a ∩ (b ∪ c))) = 1
23	1, 9	wfh1 423	. . . . . . 7 ((a ∩ (b ∪ c)) ≡ ((a ∩ b) ∪ (a ∩ c))) = 1
24	22, 23	wr2 371	. . . . . 6 (((b ∪ c) ∩ a) ≡ ((a ∩ b) ∪ (a ∩ c))) = 1
25		ancom 74	. . . . . . . 8 ((b ∪ c) ∩ a⊥ ) = (a⊥ ∩ (b ∪ c))
26	25	bi1 118	. . . . . . 7 (((b ∪ c) ∩ a⊥ ) ≡ (a⊥ ∩ (b ∪ c))) = 1
27	1	wcomcom3 416	. . . . . . . 8 C (a⊥ , b) = 1
28	9	wcomcom3 416	. . . . . . . 8 C (a⊥ , c) = 1
29	27, 28	wfh1 423	. . . . . . 7 ((a⊥ ∩ (b ∪ c)) ≡ ((a⊥ ∩ b) ∪ (a⊥ ∩ c))) = 1
30	26, 29	wr2 371	. . . . . 6 (((b ∪ c) ∩ a⊥ ) ≡ ((a⊥ ∩ b) ∪ (a⊥ ∩ c))) = 1
31	24, 30	w2or 372	. . . . 5 ((((b ∪ c) ∩ a) ∪ ((b ∪ c) ∩ a⊥ )) ≡ (((a ∩ b) ∪ (a ∩ c)) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ c)))) = 1
32	31	wr1 197	. . . 4 ((((a ∩ b) ∪ (a ∩ c)) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ c))) ≡ (((b ∪ c) ∩ a) ∪ ((b ∪ c) ∩ a⊥ ))) = 1
33	20, 32	wr2 371	. . 3 ((b ∪ c) ≡ (((b ∪ c) ∩ a) ∪ ((b ∪ c) ∩ a⊥ ))) = 1
34	33	wdf-c1 383	. 2 C ((b ∪ c), a) = 1
35	34	wcomcom 414	1 C (a, (b ∪ c)) = 1

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   C wcmtr 29

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

This theorem is referenced by:  wcom2an  428  ska2  432  ska4  433