Theorem ud3lem1a 566

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud3lem1a	((a ->3 b)' ^ (b ->3 a)) = (a ^ b')

Proof of Theorem ud3lem1a

Step	Hyp	Ref	Expression
1		ud3lem0c 279	. . 3 (a ->3 b)' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
2		df-i3 46	. . 3 (b ->3 a) = (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))
3	1, 2	2an 79	. 2 ((a ->3 b)' ^ (b ->3 a)) = ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))))
4		comor2 462	. . . . . . . . 9 (a v b') C b'
5		comor1 461	. . . . . . . . 9 (a v b') C a
6	4, 5	com2an 484	. . . . . . . 8 (a v b') C (b' ^ a)
7	5	comcom2 183	. . . . . . . . 9 (a v b') C a'
8	4, 7	com2an 484	. . . . . . . 8 (a v b') C (b' ^ a')
9	6, 8	com2or 483	. . . . . . 7 (a v b') C ((b' ^ a) v (b' ^ a'))
10	9	comcom 453	. . . . . 6 ((b' ^ a) v (b' ^ a')) C (a v b')
11		comor2 462	. . . . . . . . . 10 (a v b) C b
12	11	comcom2 183	. . . . . . . . 9 (a v b) C b'
13		comor1 461	. . . . . . . . 9 (a v b) C a
14	12, 13	com2an 484	. . . . . . . 8 (a v b) C (b' ^ a)
15	13	comcom2 183	. . . . . . . . 9 (a v b) C a'
16	12, 15	com2an 484	. . . . . . . 8 (a v b) C (b' ^ a')
17	14, 16	com2or 483	. . . . . . 7 (a v b) C ((b' ^ a) v (b' ^ a'))
18	17	comcom 453	. . . . . 6 ((b' ^ a) v (b' ^ a')) C (a v b)
19	10, 18	com2an 484	. . . . 5 ((b' ^ a) v (b' ^ a')) C ((a v b') ^ (a v b))
20		comanr2 465	. . . . . . . . 9 a C (b' ^ a)
21	20	comcom3 454	. . . . . . . 8 a' C (b' ^ a)
22		comanr2 465	. . . . . . . 8 a' C (b' ^ a')
23	21, 22	com2or 483	. . . . . . 7 a' C ((b' ^ a) v (b' ^ a'))
24	23	comcom 453	. . . . . 6 ((b' ^ a) v (b' ^ a')) C a'
25		coman2 186	. . . . . . . . 9 (a ^ b') C b'
26		coman1 185	. . . . . . . . 9 (a ^ b') C a
27	25, 26	com2an 484	. . . . . . . 8 (a ^ b') C (b' ^ a)
28	26	comcom2 183	. . . . . . . . 9 (a ^ b') C a'
29	25, 28	com2an 484	. . . . . . . 8 (a ^ b') C (b' ^ a')
30	27, 29	com2or 483	. . . . . . 7 (a ^ b') C ((b' ^ a) v (b' ^ a'))
31	30	comcom 453	. . . . . 6 ((b' ^ a) v (b' ^ a')) C (a ^ b')
32	24, 31	com2or 483	. . . . 5 ((b' ^ a) v (b' ^ a')) C (a' v (a ^ b'))
33	19, 32	com2an 484	. . . 4 ((b' ^ a) v (b' ^ a')) C (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
34		comanr1 464	. . . . . . . 8 b' C (b' ^ a)
35	34	comcom6 459	. . . . . . 7 b C (b' ^ a)
36		comanr1 464	. . . . . . . 8 b' C (b' ^ a')
37	36	comcom6 459	. . . . . . 7 b C (b' ^ a')
38	35, 37	com2or 483	. . . . . 6 b C ((b' ^ a) v (b' ^ a'))
39	38	comcom 453	. . . . 5 ((b' ^ a) v (b' ^ a')) C b
40		comor1 461	. . . . . . . 8 (b' v a) C b'
41		comor2 462	. . . . . . . 8 (b' v a) C a
42	40, 41	com2an 484	. . . . . . 7 (b' v a) C (b' ^ a)
43	41	comcom2 183	. . . . . . . 8 (b' v a) C a'
44	40, 43	com2an 484	. . . . . . 7 (b' v a) C (b' ^ a')
45	42, 44	com2or 483	. . . . . 6 (b' v a) C ((b' ^ a) v (b' ^ a'))
46	45	comcom 453	. . . . 5 ((b' ^ a) v (b' ^ a')) C (b' v a)
47	39, 46	com2an 484	. . . 4 ((b' ^ a) v (b' ^ a')) C (b ^ (b' v a))
48	33, 47	fh2 470	. . 3 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = (((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ ((b' ^ a) v (b' ^ a'))) v ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b ^ (b' v a))))
49		coman2 186	. . . . . . . . . 10 (b' ^ a) C a
50		coman1 185	. . . . . . . . . 10 (b' ^ a) C b'
51	49, 50	com2or 483	. . . . . . . . 9 (b' ^ a) C (a v b')
52	50	comcom7 460	. . . . . . . . . 10 (b' ^ a) C b
53	49, 52	com2or 483	. . . . . . . . 9 (b' ^ a) C (a v b)
54	51, 53	com2an 484	. . . . . . . 8 (b' ^ a) C ((a v b') ^ (a v b))
55	49	comcom2 183	. . . . . . . . 9 (b' ^ a) C a'
56	49, 50	com2an 484	. . . . . . . . 9 (b' ^ a) C (a ^ b')
57	55, 56	com2or 483	. . . . . . . 8 (b' ^ a) C (a' v (a ^ b'))
58	54, 57	com2an 484	. . . . . . 7 (b' ^ a) C (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
59	50, 55	com2an 484	. . . . . . 7 (b' ^ a) C (b' ^ a')
60	58, 59	fh2 470	. . . . . 6 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ ((b' ^ a) v (b' ^ a'))) = (((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a)) v ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a')))
61		anass 76	. . . . . . . . 9 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a)) = (((a v b') ^ (a v b)) ^ ((a' v (a ^ b')) ^ (b' ^ a)))
62		ancom 74	. . . . . . . . . . . 12 ((a' v (a ^ b')) ^ (b' ^ a)) = ((b' ^ a) ^ (a' v (a ^ b')))
63		ancom 74	. . . . . . . . . . . . . 14 (b' ^ a) = (a ^ b')
64		ax-a2 31	. . . . . . . . . . . . . 14 (a' v (a ^ b')) = ((a ^ b') v a')
65	63, 64	2an 79	. . . . . . . . . . . . 13 ((b' ^ a) ^ (a' v (a ^ b'))) = ((a ^ b') ^ ((a ^ b') v a'))
66		a5c 121	. . . . . . . . . . . . 13 ((a ^ b') ^ ((a ^ b') v a')) = (a ^ b')
67	65, 66	ax-r2 36	. . . . . . . . . . . 12 ((b' ^ a) ^ (a' v (a ^ b'))) = (a ^ b')
68	62, 67	ax-r2 36	. . . . . . . . . . 11 ((a' v (a ^ b')) ^ (b' ^ a)) = (a ^ b')
69	68	lan 77	. . . . . . . . . 10 (((a v b') ^ (a v b)) ^ ((a' v (a ^ b')) ^ (b' ^ a))) = (((a v b') ^ (a v b)) ^ (a ^ b'))
70		ancom 74	. . . . . . . . . . 11 (((a v b') ^ (a v b)) ^ (a ^ b')) = ((a ^ b') ^ ((a v b') ^ (a v b)))
71		lea 160	. . . . . . . . . . . . 13 (a ^ b') =< a
72		leo 158	. . . . . . . . . . . . . 14 a =< (a v b')
73		leo 158	. . . . . . . . . . . . . 14 a =< (a v b)
74	72, 73	ler2an 173	. . . . . . . . . . . . 13 a =< ((a v b') ^ (a v b))
75	71, 74	letr 137	. . . . . . . . . . . 12 (a ^ b') =< ((a v b') ^ (a v b))
76	75	df2le2 136	. . . . . . . . . . 11 ((a ^ b') ^ ((a v b') ^ (a v b))) = (a ^ b')
77	70, 76	ax-r2 36	. . . . . . . . . 10 (((a v b') ^ (a v b)) ^ (a ^ b')) = (a ^ b')
78	69, 77	ax-r2 36	. . . . . . . . 9 (((a v b') ^ (a v b)) ^ ((a' v (a ^ b')) ^ (b' ^ a))) = (a ^ b')
79	61, 78	ax-r2 36	. . . . . . . 8 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a)) = (a ^ b')
80		an32 83	. . . . . . . . 9 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a')) = ((((a v b') ^ (a v b)) ^ (b' ^ a')) ^ (a' v (a ^ b')))
81		anass 76	. . . . . . . . . . . 12 (((a v b') ^ (a v b)) ^ (b' ^ a')) = ((a v b') ^ ((a v b) ^ (b' ^ a'