Theorem u3lem13b 772

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 45	. 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 629	. . . . . 6 ((a ->3 b_|_)_|_ ^ a_|_) = (a_|_ ^ ((a v b_|_) ^ (a v b_|__|_)))
3		ax-a1 29	. . . . . . . . 9 a = a_|__|_
4	3	ax-r1 34	. . . . . . . 8 a_|__|_ = a
5	4	lan 70	. . . . . . 7 ((a ->3 b_|_)_|_ ^ a_|__|_) = ((a ->3 b_|_)_|_ ^ a)
6		u3lemnaa 624	. . . . . . 7 ((a ->3 b_|_)_|_ ^ a) = (a ^ b_|__|_)
7	5, 6	ax-r2 35	. . . . . 6 ((a ->3 b_|_)_|_ ^ a_|__|_) = (a ^ b_|__|_)
8	2, 7	2or 67	. . . . 5 (((a ->3 b_|_)_|_ ^ a_|_) v ((a ->3 b_|_)_|_ ^ a_|__|_)) = ((a_|_ ^ ((a v b_|_) ^ (a v b_|__|_))) v (a ^ b_|__|_))
9		comanr1 446	. . . . . . . 8 a C (a ^ b_|__|_)
10	9	comcom3 436	. . . . . . 7 a_|_ C (a ^ b_|__|_)
11		comorr 176	. . . . . . . . 9 a C (a v b_|_)
12		comorr 176	. . . . . . . . 9 a C (a v b_|__|_)
13	11, 12	com2an 466	. . . . . . . 8 a C ((a v b_|_) ^ (a v b_|__|_))
14	13	comcom3 436	. . . . . . 7 a_|_ C ((a v b_|_) ^ (a v b_|__|_))
15	10, 14	fh4r 458	. . . . . 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 177	. . . . . . . . . 10 (a ^ b_|__|_) C a
17		coman2 178	. . . . . . . . . . 11 (a ^ b_|__|_) C b_|__|_
18	17	comcom7 442	. . . . . . . . . 10 (a ^ b_|__|_) C b_|_
19	16, 18	com2or 465	. . . . . . . . 9 (a ^ b_|__|_) C (a v b_|_)
20	16, 17	com2or 465	. . . . . . . . 9 (a ^ b_|__|_) C (a v b_|__|_)
21	19, 20	fh3r 457	. . . . . . . 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 70	. . . . . . 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 30	. . . . . . . . . . . 12 ((a v b_|_) v (a ^ b_|__|_)) = ((a ^ b_|__|_) v (a v b_|_))
24		lea 152	. . . . . . . . . . . . . 14 (a ^ b_|__|_) =< a
25		leo 150	. . . . . . . . . . . . . 14 a =< (a v b_|_)
26	24, 25	letr 129	. . . . . . . . . . . . 13 (a ^ b_|__|_) =< (a v b_|_)
27	26	df-le2 123	. . . . . . . . . . . 12 ((a ^ b_|__|_) v (a v b_|_)) = (a v b_|_)
28	23, 27	ax-r2 35	. . . . . . . . . . 11 ((a v b_|_) v (a ^ b_|__|_)) = (a v b_|_)
29		ax-a2 30	. . . . . . . . . . . 12 ((a v b_|__|_) v (a ^ b_|__|_)) = ((a ^ b_|__|_) v (a v b_|__|_))
30		leo 150	. . . . . . . . . . . . . 14 a =< (a v b_|__|_)
31	24, 30	letr 129	. . . . . . . . . . . . 13 (a ^ b_|__|_) =< (a v b_|__|_)
32	31	df-le2 123	. . . . . . . . . . . 12 ((a ^ b_|__|_) v (a v b_|__|_)) = (a v b_|__|_)
33	29, 32	ax-r2 35	. . . . . . . . . . 11 ((a v b_|__|_) v (a ^ b_|__|_)) = (a v b_|__|_)
34	28, 33	2an 72	. . . . . . . . . 10 (((a v b_|_) v (a ^ b_|__|_)) ^ ((a v b_|__|_) v (a ^ b_|__|_))) = ((a v b_|_) ^ (a v b_|__|_))
35		id 58	. . . . . . . . . 10 ((a v b_|_) ^ (a v b_|__|_)) = ((a v b_|_) ^ (a v b_|__|_))
36	34, 35	ax-r2 35	. . . . . . . . 9 (((a v b_|_) v (a ^ b_|__|_)) ^ ((a v b_|__|_) v (a ^ b_|__|_))) = ((a v b_|_) ^ (a v b_|__|_))
37	36	lan 70	. . . . . . . 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 58	. . . . . . . 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 35	. . . . . . 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 35	. . . . . 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 35	. . . . 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 35	. . . 4 (((a ->3 b_|_)_|_ ^ a_|_) v ((a ->3 b_|_)_|_ ^ a_|__|_)) = ((a_|_ v (a ^ b_|__|_)) ^ ((a v b_|_) ^ (a v b_|__|_)))
43		u3lemnona 649	. . . . . 6 ((a ->3 b_|_)_|_ v a_|_) = (a_|_ v (a ^ b_|__|_))
44	43	lan 70	. . . . 5 ((a ->3 b_|_) ^ ((a ->3 b_|_)_|_ v a_|_)) = ((a ->3 b_|_) ^ (a_|_ v (a ^ b_|__|_)))
45		comi31 490	. . . . . . . 8 a C (a ->3 b_|_)
46	45	comcom3 436	. . . . . . 7 a_|_ C (a ->3 b_|_)
47	46, 10	fh2 452	. . . . . 6 ((a ->3 b_|_) ^ (a_|_ v (a ^ b_|__|_))) = (((a ->3 b_|_) ^ a_|_) v ((a ->3 b_|_) ^ (a ^ b_|__|_)))
48		u3lemana 589	. . . . . . . 8 ((a ->3 b_|_) ^ a_|_) = ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))
49		anandi 106	. . . . . . . . 9 ((a ->3 b_|_) ^ (a ^ b_|__|_)) = (((a ->3 b_|_) ^ a) ^ ((a ->3 b_|_) ^ b_|__|_))
50		u3lemaa 584	. . . . . . . . . . 11 ((a ->3 b_|_) ^ a) = (a ^ (a_|_ v b_|_))
51		u3lemanb 599	. . . . . . . . . . 11 ((a ->3 b_|_) ^ b_|__|_) = (a_|_ ^ b_|__|_)
52	50, 51	2an 72	. . . . . . . . . 10 (((a ->3 b_|_) ^ a) ^ ((a ->3 b_|_) ^ b_|__|_)) = ((a ^ (a_|_ v b_|_)) ^ (a_|_ ^ b_|__|_))
53		an4 78	. . . . . . . . . . 11 ((a ^ (a_|_ v b_|_)) ^ (a_|_ ^ b_|__|_)) = ((a ^ a_|_) ^ ((a_|_ v b_|_) ^ b_|__|_))
54		ancom 68	. . . . . . . . . . . 12 ((a ^ a_|_) ^ ((a_|_ v b_|_) ^ b_|__|_)) = (((a_|_ v b_|_) ^ b_|__|_) ^ (a ^ a_|_))
55		dff 93	. . . . . . . . . . . . . . 15 0 = (a ^ a_|_)
56	55	ax-r1 34	. . . . . . . . . . . . . 14 (a ^ a_|_) = 0
57	56	lan 70	. . . . . . . . . . . . 13 (((a_|_ v b_|_) ^ b_|__|_) ^ (a ^ a_|_)) = (((a_|_ v b_|_) ^ b_|__|_) ^ 0)
58		an0 100	. . . . . . . . . . . . 13 (((a_|_ v b_|_) ^ b_|__|_) ^ 0) = 0
59	57, 58	ax-r2 35	. . . . . . . . . . . 12 (((a_|_ v b_|_) ^ b_|__|_) ^ (a ^ a_|_)) = 0
60	54, 59	ax-r2 35	. . . . . . . . . . 11 ((a ^ a_|_) ^ ((a_|_ v b_|_) ^ b_|__|_)) = 0
61	53, 60	ax-r2 35	. . . . . . . . . 10 ((a ^ (a_|_ v b_|_)) ^ (a_|_ ^ b_|__|_)) = 0
62	52, 61	ax-r2 35	. . . . . . . . 9 (((a ->3 b_|_) ^ a) ^ ((a ->3 b_|_) ^ b_|__|_)) = 0
63	49, 62	ax-r2 35	. . . . . . . 8 ((a ->3 b_|_) ^ (a ^ b_|__|_)) = 0
64	48, 63	2or 67	. . . . . . 7 (((a ->3 b_|_) ^ a_|_) v ((a ->3 b_|_) ^ (a ^ b_|__|_))) = (((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)) v 0)
65		or0 94	. . . . . . 7 (((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)) v 0) = ((a_|_ ^ b_|_) v (