Theorem u3lem13b 790

Description: Lemma for unified implication study.

Assertion

Ref	Expression
u3lem13b	((a ->3 b') ->3 a') = (a ->1 b)

Proof of Theorem u3lem13b

Step	Hyp	Ref	Expression
1		df-i3 46	. 2 ((a ->3 b') ->3 a') = ((((a ->3 b')' ^ a') v ((a ->3 b')' ^ a'')) v ((a ->3 b') ^ ((a ->3 b')' v a')))
2		u3lemnana 647	. . . . . 6 ((a ->3 b')' ^ a') = (a' ^ ((a v b') ^ (a v b'')))
3		ax-a1 30	. . . . . . . . 9 a = a''
4	3	ax-r1 35	. . . . . . . 8 a'' = a
5	4	lan 77	. . . . . . 7 ((a ->3 b')' ^ a'') = ((a ->3 b')' ^ a)
6		u3lemnaa 642	. . . . . . 7 ((a ->3 b')' ^ a) = (a ^ b'')
7	5, 6	ax-r2 36	. . . . . 6 ((a ->3 b')' ^ a'') = (a ^ b'')
8	2, 7	2or 72	. . . . 5 (((a ->3 b')' ^ a') v ((a ->3 b')' ^ a'')) = ((a' ^ ((a v b') ^ (a v b''))) v (a ^ b''))
9		comanr1 464	. . . . . . . 8 a C (a ^ b'')
10	9	comcom3 454	. . . . . . 7 a' C (a ^ b'')
11		comorr 184	. . . . . . . . 9 a C (a v b')
12		comorr 184	. . . . . . . . 9 a C (a v b'')
13	11, 12	com2an 484	. . . . . . . 8 a C ((a v b') ^ (a v b''))
14	13	comcom3 454	. . . . . . 7 a' C ((a v b') ^ (a v b''))
15	10, 14	fh4r 476	. . . . . 6 ((a' ^ ((a v b') ^ (a v b''))) v (a ^ b'')) = ((a' v (a ^ b'')) ^ (((a v b') ^ (a v b'')) v (a ^ b'')))
16		coman1 185	. . . . . . . . . 10 (a ^ b'') C a
17		coman2 186	. . . . . . . . . . 11 (a ^ b'') C b''
18	17	comcom7 460	. . . . . . . . . 10 (a ^ b'') C b'
19	16, 18	com2or 483	. . . . . . . . 9 (a ^ b'') C (a v b')
20	16, 17	com2or 483	. . . . . . . . 9 (a ^ b'') C (a v b'')
21	19, 20	fh3r 475	. . . . . . . 8 (((a v b') ^ (a v b'')) v (a ^ b'')) = (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b'')))
22	21	lan 77	. . . . . . 7 ((a' v (a ^ b'')) ^ (((a v b') ^ (a v b'')) v (a ^ b''))) = ((a' v (a ^ b'')) ^ (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b''))))
23		ax-a2 31	. . . . . . . . . . . 12 ((a v b') v (a ^ b'')) = ((a ^ b'') v (a v b'))
24		lea 160	. . . . . . . . . . . . . 14 (a ^ b'') =< a
25		leo 158	. . . . . . . . . . . . . 14 a =< (a v b')
26	24, 25	letr 137	. . . . . . . . . . . . 13 (a ^ b'') =< (a v b')
27	26	df-le2 131	. . . . . . . . . . . 12 ((a ^ b'') v (a v b')) = (a v b')
28	23, 27	ax-r2 36	. . . . . . . . . . 11 ((a v b') v (a ^ b'')) = (a v b')
29		ax-a2 31	. . . . . . . . . . . 12 ((a v b'') v (a ^ b'')) = ((a ^ b'') v (a v b''))
30		leo 158	. . . . . . . . . . . . . 14 a =< (a v b'')
31	24, 30	letr 137	. . . . . . . . . . . . 13 (a ^ b'') =< (a v b'')
32	31	df-le2 131	. . . . . . . . . . . 12 ((a ^ b'') v (a v b'')) = (a v b'')
33	29, 32	ax-r2 36	. . . . . . . . . . 11 ((a v b'') v (a ^ b'')) = (a v b'')
34	28, 33	2an 79	. . . . . . . . . 10 (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b''))) = ((a v b') ^ (a v b''))
35		id 59	. . . . . . . . . 10 ((a v b') ^ (a v b'')) = ((a v b') ^ (a v b''))
36	34, 35	ax-r2 36	. . . . . . . . 9 (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b''))) = ((a v b') ^ (a v b''))
37	36	lan 77	. . . . . . . 8 ((a' v (a ^ b'')) ^ (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b'')))) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
38		id 59	. . . . . . . 8 ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b''))) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
39	37, 38	ax-r2 36	. . . . . . 7 ((a' v (a ^ b'')) ^ (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b'')))) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
40	22, 39	ax-r2 36	. . . . . 6 ((a' v (a ^ b'')) ^ (((a v b') ^ (a v b'')) v (a ^ b''))) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
41	15, 40	ax-r2 36	. . . . 5 ((a' ^ ((a v b') ^ (a v b''))) v (a ^ b'')) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
42	8, 41	ax-r2 36	. . . 4 (((a ->3 b')' ^ a') v ((a ->3 b')' ^ a'')) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
43		u3lemnona 667	. . . . . 6 ((a ->3 b')' v a') = (a' v (a ^ b''))
44	43	lan 77	. . . . 5 ((a ->3 b') ^ ((a ->3 b')' v a')) = ((a ->3 b') ^ (a' v (a ^ b'')))
45		comi31 508	. . . . . . . 8 a C (a ->3 b')
46	45	comcom3 454	. . . . . . 7 a' C (a ->3 b')
47	46, 10	fh2 470	. . . . . 6 ((a ->3 b') ^ (a' v (a ^ b''))) = (((a ->3 b') ^ a') v ((a ->3 b') ^ (a ^ b'')))
48		u3lemana 607	. . . . . . . 8 ((a ->3 b') ^ a') = ((a' ^ b') v (a' ^ b''))
49		anandi 114	. . . . . . . . 9 ((a ->3 b') ^ (a ^ b'')) = (((a ->3 b') ^ a) ^ ((a ->3 b') ^ b''))
50		u3lemaa 602	. . . . . . . . . . 11 ((a ->3 b') ^ a) = (a ^ (a' v b'))
51		u3lemanb 617	. . . . . . . . . . 11 ((a ->3 b') ^ b'') = (a' ^ b'')
52	50, 51	2an 79	. . . . . . . . . 10 (((a ->3 b') ^ a) ^ ((a ->3 b') ^ b'')) = ((a ^ (a' v b')) ^ (a' ^ b''))
53		an4 86	. . . . . . . . . . 11 ((a ^ (a' v b')) ^ (a' ^ b'')) = ((a ^ a') ^ ((a' v b') ^ b''))
54		ancom 74	. . . . . . . . . . . 12 ((a ^ a') ^ ((a' v b') ^ b'')) = (((a' v b') ^ b'') ^ (a ^ a'))
55		dff 101	. . . . . . . . . . . . . . 15 0 = (a ^ a')
56	55	ax-r1 35	. . . . . . . . . . . . . 14 (a ^ a') = 0
57	56	lan 77	. . . . . . . . . . . . 13 (((a' v b') ^ b'') ^ (a ^ a')) = (((a' v b') ^ b'') ^ 0)
58		an0 108	. . . . . . . . . . . . 13 (((a' v b') ^ b'') ^ 0) = 0
59	57, 58	ax-r2 36	. . . . . . . . . . . 12 (((a' v b') ^ b'') ^ (a ^ a')) = 0
60	54, 59	ax-r2 36	. . . . . . . . . . 11 ((a ^ a') ^ ((a' v b') ^ b'')) = 0
61	53, 60	ax-r2 36	. . . . . . . . . 10 ((a ^ (a' v b')) ^ (a' ^ b'')) = 0
62	52, 61	ax-r2 36	. . . . . . . . 9 (((a ->3 b') ^ a) ^ ((a ->3 b') ^ b'')) = 0
63	49, 62	ax-r2 36	. . . . . . . 8 ((a ->3 b') ^ (a ^ b'')) = 0
64	48, 63	2or 72	. . . . . . 7 (((a ->3 b') ^ a') v ((a ->3 b') ^ (a ^ b''))) = (((a' ^ b') v (a' ^ b'')) v 0)
65		or0 102	. . . . . . 7 (