Theorem ud3lem1b 549

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud3lem1b	((a ->3 b)_|_ ^ (b ->3 a)_|_) = 0

Proof of Theorem ud3lem1b

Step	Hyp	Ref	Expression
1		ud3lem0c 271	. . 3 (a ->3 b)_|_ = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))
2		ud3lem0c 271	. . 3 (b ->3 a)_|_ = (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))
3	1, 2	2an 72	. 2 ((a ->3 b)_|_ ^ (b ->3 a)_|_) = ((((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_))) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_))))
4		an32 76	. . 3 ((((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_))) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))) = ((((a v b_|_) ^ (a v b)) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))) ^ (a_|_ v (a ^ b_|_)))
5		an32 76	. . . . . 6 (((a v b_|_) ^ (a v b)) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))) = (((a v b_|_) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))) ^ (a v b))
6		an12 74	. . . . . . . . 9 ((a v b_|_) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))) = (((b v a_|_) ^ (b v a)) ^ ((a v b_|_) ^ (b_|_ v (b ^ a_|_))))
7		comor2 444	. . . . . . . . . . . . 13 (a v b_|_) C b_|_
8	7	comcom7 442	. . . . . . . . . . . . . 14 (a v b_|_) C b
9		comor1 443	. . . . . . . . . . . . . . 15 (a v b_|_) C a
10	9	comcom2 175	. . . . . . . . . . . . . 14 (a v b_|_) C a_|_
11	8, 10	com2an 466	. . . . . . . . . . . . 13 (a v b_|_) C (b ^ a_|_)
12	7, 11	fh1 451	. . . . . . . . . . . 12 ((a v b_|_) ^ (b_|_ v (b ^ a_|_))) = (((a v b_|_) ^ b_|_) v ((a v b_|_) ^ (b ^ a_|_)))
13		ancom 68	. . . . . . . . . . . . . . . 16 ((a v b_|_) ^ b_|_) = (b_|_ ^ (a v b_|_))
14		ax-a2 30	. . . . . . . . . . . . . . . . 17 (a v b_|_) = (b_|_ v a)
15	14	lan 70	. . . . . . . . . . . . . . . 16 (b_|_ ^ (a v b_|_)) = (b_|_ ^ (b_|_ v a))
16	13, 15	ax-r2 35	. . . . . . . . . . . . . . 15 ((a v b_|_) ^ b_|_) = (b_|_ ^ (b_|_ v a))
17		a5c 113	. . . . . . . . . . . . . . 15 (b_|_ ^ (b_|_ v a)) = b_|_
18	16, 17	ax-r2 35	. . . . . . . . . . . . . 14 ((a v b_|_) ^ b_|_) = b_|_
19		anor1 80	. . . . . . . . . . . . . . . 16 (b ^ a_|_) = (b_|_ v a)_|_
20	14, 19	2an 72	. . . . . . . . . . . . . . 15 ((a v b_|_) ^ (b ^ a_|_)) = ((b_|_ v a) ^ (b_|_ v a)_|_)
21		dff 93	. . . . . . . . . . . . . . . 16 0 = ((b_|_ v a) ^ (b_|_ v a)_|_)
22	21	ax-r1 34	. . . . . . . . . . . . . . 15 ((b_|_ v a) ^ (b_|_ v a)_|_) = 0
23	20, 22	ax-r2 35	. . . . . . . . . . . . . 14 ((a v b_|_) ^ (b ^ a_|_)) = 0
24	18, 23	2or 67	. . . . . . . . . . . . 13 (((a v b_|_) ^ b_|_) v ((a v b_|_) ^ (b ^ a_|_))) = (b_|_ v 0)
25		or0 94	. . . . . . . . . . . . 13 (b_|_ v 0) = b_|_
26	24, 25	ax-r2 35	. . . . . . . . . . . 12 (((a v b_|_) ^ b_|_) v ((a v b_|_) ^ (b ^ a_|_))) = b_|_
27	12, 26	ax-r2 35	. . . . . . . . . . 11 ((a v b_|_) ^ (b_|_ v (b ^ a_|_))) = b_|_
28	27	lan 70	. . . . . . . . . 10 (((b v a_|_) ^ (b v a)) ^ ((a v b_|_) ^ (b_|_ v (b ^ a_|_)))) = (((b v a_|_) ^ (b v a)) ^ b_|_)
29		ancom 68	. . . . . . . . . . 11 (((b v a_|_) ^ (b v a)) ^ b_|_) = (b_|_ ^ ((b v a_|_) ^ (b v a)))
30		anass 69	. . . . . . . . . . . 12 ((b_|_ ^ (b v a_|_)) ^ (b v a)) = (b_|_ ^ ((b v a_|_) ^ (b v a)))
31	30	ax-r1 34	. . . . . . . . . . 11 (b_|_ ^ ((b v a_|_) ^ (b v a))) = ((b_|_ ^ (b v a_|_)) ^ (b v a))
32	29, 31	ax-r2 35	. . . . . . . . . 10 (((b v a_|_) ^ (b v a)) ^ b_|_) = ((b_|_ ^ (b v a_|_)) ^ (b v a))
33	28, 32	ax-r2 35	. . . . . . . . 9 (((b v a_|_) ^ (b v a)) ^ ((a v b_|_) ^ (b_|_ v (b ^ a_|_)))) = ((b_|_ ^ (b v a_|_)) ^ (b v a))
34	6, 33	ax-r2 35	. . . . . . . 8 ((a v b_|_) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))) = ((b_|_ ^ (b v a_|_)) ^ (b v a))
35	34	ran 71	. . . . . . 7 (((a v b_|_) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))) ^ (a v b)) = (((b_|_ ^ (b v a_|_)) ^ (b v a)) ^ (a v b))
36		ax-a2 30	. . . . . . . . 9 (a v b) = (b v a)
37	36	lan 70	. . . . . . . 8 (((b_|_ ^ (b v a_|_)) ^ (b v a)) ^ (a v b)) = (((b_|_ ^ (b v a_|_)) ^ (b v a)) ^ (b v a))
38		anass 69	. . . . . . . . 9 (((b_|_ ^ (b v a_|_)) ^ (b v a)) ^ (b v a)) = ((b_|_ ^ (b v a_|_)) ^ ((b v a) ^ (b v a)))
39		anidm 103	. . . . . . . . . . 11 ((b v a) ^ (b v a)) = (b v a)
40	39	lan 70	. . . . . . . . . 10 ((b_|_ ^ (b v a_|_)) ^ ((b v a) ^ (b v a))) = ((b_|_ ^ (b v a_|_)) ^ (b v a))
41		an32 76	. . . . . . . . . 10 ((b_|_ ^ (b v a_|_)) ^ (b v a)) = ((b_|_ ^ (b v a)) ^ (b v a_|_))
42	40, 41	ax-r2 35	. . . . . . . . 9 ((b_|_ ^ (b v a_|_)) ^ ((b v a) ^ (b v a))) = ((b_|_ ^ (b v a)) ^ (b v a_|_))
43	38, 42	ax-r2 35	. . . . . . . 8 (((b_|_ ^ (b v a_|_)) ^ (b v a)) ^ (b v a)) = ((b_|_ ^ (b v a)) ^ (b v a_|_))
44	37, 43	ax-r2 35	. . . . . . 7 (((b_|_ ^ (b v a_|_)) ^ (b v a)) ^ (a v b)) = ((b_|_ ^ (b v a)) ^ (b v a_|_))
45	35, 44	ax-r2 35	. . . . . 6 (((a v b_|_) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))) ^ (a v b)) = ((b_|_ ^ (b v a)) ^ (b v a_|_))
46	5, 45	ax-r2 35	. . . . 5 (((a v b_|_) ^ (a v b)) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))) = ((b_|_ ^ (b v a)) ^ (b v a_|_))
47	46	ran 71	. . . 4 ((((a v b_|_) ^ (a v b)) ^ (((b v a_|_) ^ (b v a)) ^ (b_|_ v (b ^ a_|_)))) ^ (a_|_ v (a ^ b_|_))) = (((b_|_ ^ (b v a)) ^ (b v a_|_)) ^ (a_|_ v (a ^ b_|_)))
48		anass 69	. . . . 5 (((b_|_ ^ (b v a)) ^ (b v a_|_)) ^ (a_|_ v (a ^ b_|_))) = ((b_|_ ^ (b v a)) ^ ((b v a_|_) ^ (a_|_ v (a ^ b_|_))))
49		ax-a2 30	. . . . . . . . 9 (b v a_|_) = (a_|_ v b)
50	49	ran 71	. . . . . . . 8 ((b v a_|_) ^ (a_|_ v (a ^ b_|_))) = ((a_|_ v b) ^ (a_|_ v (a ^ b_|_)))
51		ancom 68	. . . . . . . . 9 ((a_|_ v b) ^ (a_|_ v (a ^ b_|_))) = ((a_|_ v (a ^ b_|_)) ^ (a_|_ v b))
52		comor1 443	. . . . . . . . . . 11 (a_|_ v b) C a_|_
53	52	comcom7 442	. . . . . . . . . . . 12 (a_|_ v b) C a
54		comor2 444	. . . . . . . . . . . . 13 (a_|_ v b) C b
55	54	comcom2 175	. . . . . . . . . . . 12 (a_|_ v b) C b_|_
56	53, 55	com2an 466	. . . . . . . . . . 11 (a_|_ v b) C (a ^ b_|_)
57	52, 56	fh1r 455	. . . . . . . . . 10 ((a_|_ v (a ^ b_|_)) ^ (a_|_ v b)) = ((a_|_ ^ (a_|_ v b)) v ((a ^ b_|_) ^ (a_|_ v b)))
58		a5c 113	. . . . . . . . . . . 12 (a_|_