Theorem ud3lem3 576

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud3lem3	((a ->3 b) ->3 (a v b)) = (a v b)

Proof of Theorem ud3lem3

Step	Hyp	Ref	Expression
1		df-i3 46	. 2 ((a ->3 b) ->3 (a v b)) = ((((a ->3 b)' ^ (a v b)) v ((a ->3 b)' ^ (a v b)')) v ((a ->3 b) ^ ((a ->3 b)' v (a v b))))
2		ud3lem3a 572	. . . . . . 7 ((a ->3 b)' ^ (a v b)) = (a ->3 b)'
3		ud3lem0c 279	. . . . . . 7 (a ->3 b)' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
4	2, 3	ax-r2 36	. . . . . 6 ((a ->3 b)' ^ (a v b)) = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
5		ud3lem3b 573	. . . . . 6 ((a ->3 b)' ^ (a v b)') = 0
6	4, 5	2or 72	. . . . 5 (((a ->3 b)' ^ (a v b)) v ((a ->3 b)' ^ (a v b)')) = ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v 0)
7		or0 102	. . . . 5 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v 0) = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
8	6, 7	ax-r2 36	. . . 4 (((a ->3 b)' ^ (a v b)) v ((a ->3 b)' ^ (a v b)')) = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
9		ud3lem3d 575	. . . 4 ((a ->3 b) ^ ((a ->3 b)' v (a v b))) = ((a' ^ b) v (a ^ (a' v b)))
10	8, 9	2or 72	. . 3 ((((a ->3 b)' ^ (a v b)) v ((a ->3 b)' ^ (a v b)')) v ((a ->3 b) ^ ((a ->3 b)' v (a v b)))) = ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v ((a' ^ b) v (a ^ (a' v b))))
11		coman1 185	. . . . . . . . . 10 (a' ^ b) C a'
12	11	comcom7 460	. . . . . . . . 9 (a' ^ b) C a
13		coman2 186	. . . . . . . . . 10 (a' ^ b) C b
14	13	comcom2 183	. . . . . . . . 9 (a' ^ b) C b'
15	12, 14	com2or 483	. . . . . . . 8 (a' ^ b) C (a v b')
16	12, 13	com2or 483	. . . . . . . 8 (a' ^ b) C (a v b)
17	15, 16	com2an 484	. . . . . . 7 (a' ^ b) C ((a v b') ^ (a v b))
18	17	comcom 453	. . . . . 6 ((a v b') ^ (a v b)) C (a' ^ b)
19		comorr 184	. . . . . . . . 9 a C (a v b')
20		comorr 184	. . . . . . . . 9 a C (a v b)
21	19, 20	com2an 484	. . . . . . . 8 a C ((a v b') ^ (a v b))
22	21	comcom 453	. . . . . . 7 ((a v b') ^ (a v b)) C a
23		comor1 461	. . . . . . . . . . 11 (a' v b) C a'
24	23	comcom7 460	. . . . . . . . . 10 (a' v b) C a
25		comor2 462	. . . . . . . . . . 11 (a' v b) C b
26	25	comcom2 183	. . . . . . . . . 10 (a' v b) C b'
27	24, 26	com2or 483	. . . . . . . . 9 (a' v b) C (a v b')
28	24, 25	com2or 483	. . . . . . . . 9 (a' v b) C (a v b)
29	27, 28	com2an 484	. . . . . . . 8 (a' v b) C ((a v b') ^ (a v b))
30	29	comcom 453	. . . . . . 7 ((a v b') ^ (a v b)) C (a' v b)
31	22, 30	com2an 484	. . . . . 6 ((a v b') ^ (a v b)) C (a ^ (a' v b))
32	18, 31	com2or 483	. . . . 5 ((a v b') ^ (a v b)) C ((a' ^ b) v (a ^ (a' v b)))
33	19	comcom3 454	. . . . . . . 8 a' C (a v b')
34	20	comcom3 454	. . . . . . . 8 a' C (a v b)
35	33, 34	com2an 484	. . . . . . 7 a' C ((a v b') ^ (a v b))
36	35	comcom 453	. . . . . 6 ((a v b') ^ (a v b)) C a'
37		coman1 185	. . . . . . . . 9 (a ^ b') C a
38		coman2 186	. . . . . . . . 9 (a ^ b') C b'
39	37, 38	com2or 483	. . . . . . . 8 (a ^ b') C (a v b')
40	38	comcom7 460	. . . . . . . . 9 (a ^ b') C b
41	37, 40	com2or 483	. . . . . . . 8 (a ^ b') C (a v b)
42	39, 41	com2an 484	. . . . . . 7 (a ^ b') C ((a v b') ^ (a v b))
43	42	comcom 453	. . . . . 6 ((a v b') ^ (a v b)) C (a ^ b')
44	36, 43	com2or 483	. . . . 5 ((a v b') ^ (a v b)) C (a' v (a ^ b'))
45	32, 44	fh4r 476	. . . 4 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v ((a' ^ b) v (a ^ (a' v b)))) = ((((a v b') ^ (a v b)) v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a' v (a ^ b')) v ((a' ^ b) v (a ^ (a' v b)))))
46		comor1 461	. . . . . . . . . . 11 (a v b') C a
47	46	comcom2 183	. . . . . . . . . 10 (a v b') C a'
48		comor2 462	. . . . . . . . . . 11 (a v b') C b'
49	48	comcom7 460	. . . . . . . . . 10 (a v b') C b
50	47, 49	com2an 484	. . . . . . . . 9 (a v b') C (a' ^ b)
51	47, 49	com2or 483	. . . . . . . . . 10 (a v b') C (a' v b)
52	46, 51	com2an 484	. . . . . . . . 9 (a v b') C (a ^ (a' v b))
53	50, 52	com2or 483	. . . . . . . 8 (a v b') C ((a' ^ b) v (a ^ (a' v b)))
54	46, 49	com2or 483	. . . . . . . 8 (a v b') C (a v b)
55	53, 54	fh4r 476	. . . . . . 7 (((a v b') ^ (a v b)) v ((a' ^ b) v (a ^ (a' v b)))) = (((a v b') v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a v b) v ((a' ^ b) v (a ^ (a' v b)))))
56		ax-a3 32	. . . . . . . . . . 11 (((a v b') v (a' ^ b)) v (a ^ (a' v b))) = ((a v b') v ((a' ^ b) v (a ^ (a' v b))))
57	56	ax-r1 35	. . . . . . . . . 10 ((a v b') v ((a' ^ b) v (a ^ (a' v b)))) = (((a v b') v (a' ^ b)) v (a ^ (a' v b)))
58		anor2 89	. . . . . . . . . . . . . 14 (a' ^ b) = (a v b')'
59	58	lor 70	. . . . . . . . . . . . 13 ((a v b') v (a' ^ b)) = ((a v b') v (a v b')')
60		df-t 41	. . . . . . . . . . . . . 14 1 = ((a v b') v (a v b')')
61	60	ax-r1 35	. . . . . . . . . . . . 13 ((a v b') v (a v b')') = 1
62	59, 61	ax-r2 36	. . . . . . . . . . . 12 ((a v b') v (a' ^ b)) = 1
63	62	ax-r5 38	. . . . . . . . . . 11 (((a v b') v (a' ^ b)) v (a ^ (a' v b))) = (1 v (a ^ (a' v b)))
64		or1r 105	. . . . . . . . . . 11 (1 v (a ^ (a' v b))) = 1
65	63, 64	ax-r2 36	. . . . . . . . . 10 (((a v b') v (a' ^ b)) v (a ^ (a' v b))) = 1
66	57, 65	ax-r2 36	. . . . . . . . 9 ((a v b') v ((a' ^ b) v (a ^ (a' v b)))) = 1
67		ax-a2 31	. . . . . . . . . 10 ((a v b) v ((a' ^ b) v (a ^ (a' v b)))) = (((a' ^ b) v (a ^ (a' v b))) v (a v b))
68		lear 161	. . . . . . . . . . . . 13 (a' ^ b) =< b
69		leor 159	. . . . . . . . . . . . 13 b =< (a v b)
70	68, 69	letr 137	. . . . . . . . . . . 12 (a' ^ b) =< (a v b)
71		lea 160	. . . . . . . . . . . . 13 (a ^ (a' v b)) =< a
72		leo 158	. . . . . . . . . . . . 13 a =< (a v b)
73	71, 72	letr 137	. . . . . . . . . . . 12 (a ^ (a' v b)) =< (a v b)
74	70, 73	lel2or 170	. . . . . . . . . . 11 ((a' ^ b) v (a ^ (a' v b))) =< (a v b)
75	74	df-le2 131	. . . . . . . . . 10 (((a' ^ b) v (a ^ (a' v b))) v (a v b)) = (a v b)
76	67, 75	ax-r2 36	. . . . . . . . 9 ((a v b) v ((a' ^ b) v (a ^ (a' v b)))) = (a v b)
77	66, 76	2an 79	. . . . . . . 8 (((a v b') v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a v b) v ((a' ^ b) v (a ^ (a' v b))))) = (1 ^ (a v b))
78		an1r 107	. . . . . . . 8 (1 ^ (a v b)) = (a v b)
79	77, 78	ax-r2 36	. . . . . . 7 (((a v b') v ((a' ^