Theorem u3lem13a 771

Description: Lemma for unified implication study.

Assertion

Ref	Expression
u3lem13a	(a ->3 (a ->3 b_|_)_|_) = (a ->1 b)

Proof of Theorem u3lem13a

Step	Hyp	Ref	Expression
1		df-i3 45	. 2 (a ->3 (a ->3 b_|_)_|_) = (((a_|_ ^ (a ->3 b_|_)_|_) v (a_|_ ^ (a ->3 b_|_)_|__|_)) v (a ^ (a_|_ v (a ->3 b_|_)_|_)))
2		ancom 68	. . . . . . 7 (a_|_ ^ (a ->3 b_|_)_|_) = ((a ->3 b_|_)_|_ ^ a_|_)
3		u3lemnana 629	. . . . . . 7 ((a ->3 b_|_)_|_ ^ a_|_) = (a_|_ ^ ((a v b_|_) ^ (a v b_|__|_)))
4	2, 3	ax-r2 35	. . . . . 6 (a_|_ ^ (a ->3 b_|_)_|_) = (a_|_ ^ ((a v b_|_) ^ (a v b_|__|_)))
5		ax-a1 29	. . . . . . . . 9 (a ->3 b_|_) = (a ->3 b_|_)_|__|_
6	5	ax-r1 34	. . . . . . . 8 (a ->3 b_|_)_|__|_ = (a ->3 b_|_)
7	6	lan 70	. . . . . . 7 (a_|_ ^ (a ->3 b_|_)_|__|_) = (a_|_ ^ (a ->3 b_|_))
8		ancom 68	. . . . . . . 8 (a_|_ ^ (a ->3 b_|_)) = ((a ->3 b_|_) ^ a_|_)
9		u3lemana 589	. . . . . . . 8 ((a ->3 b_|_) ^ a_|_) = ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))
10	8, 9	ax-r2 35	. . . . . . 7 (a_|_ ^ (a ->3 b_|_)) = ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))
11	7, 10	ax-r2 35	. . . . . 6 (a_|_ ^ (a ->3 b_|_)_|__|_) = ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))
12	4, 11	2or 67	. . . . 5 ((a_|_ ^ (a ->3 b_|_)_|_) v (a_|_ ^ (a ->3 b_|_)_|__|_)) = ((a_|_ ^ ((a v b_|_) ^ (a v b_|__|_))) v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)))
13		comanr1 446	. . . . . . . 8 a_|_ C (a_|_ ^ b_|_)
14		comanr1 446	. . . . . . . 8 a_|_ C (a_|_ ^ b_|__|_)
15	13, 14	com2or 465	. . . . . . 7 a_|_ C ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))
16		comorr 176	. . . . . . . . 9 a C (a v b_|_)
17		comorr 176	. . . . . . . . 9 a C (a v b_|__|_)
18	16, 17	com2an 466	. . . . . . . 8 a C ((a v b_|_) ^ (a v b_|__|_))
19	18	comcom3 436	. . . . . . 7 a_|_ C ((a v b_|_) ^ (a v b_|__|_))
20	15, 19	fh4r 458	. . . . . 6 ((a_|_ ^ ((a v b_|_) ^ (a v b_|__|_))) v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))) = ((a_|_ v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))) ^ (((a v b_|_) ^ (a v b_|__|_)) v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))))
21		ax-a2 30	. . . . . . . . 9 (a_|_ v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))) = (((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)) v a_|_)
22		lea 152	. . . . . . . . . . 11 (a_|_ ^ b_|_) =< a_|_
23		lea 152	. . . . . . . . . . 11 (a_|_ ^ b_|__|_) =< a_|_
24	22, 23	lel2or 162	. . . . . . . . . 10 ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)) =< a_|_
25	24	df-le2 123	. . . . . . . . 9 (((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)) v a_|_) = a_|_
26	21, 25	ax-r2 35	. . . . . . . 8 (a_|_ v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))) = a_|_
27		anor2 81	. . . . . . . . . . . . 13 (a_|_ ^ b_|_) = (a v b_|__|_)_|_
28		anor3 82	. . . . . . . . . . . . 13 (a_|_ ^ b_|__|_) = (a v b_|_)_|_
29	27, 28	2or 67	. . . . . . . . . . . 12 ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)) = ((a v b_|__|_)_|_ v (a v b_|_)_|_)
30		ax-a2 30	. . . . . . . . . . . 12 ((a v b_|__|_)_|_ v (a v b_|_)_|_) = ((a v b_|_)_|_ v (a v b_|__|_)_|_)
31	29, 30	ax-r2 35	. . . . . . . . . . 11 ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)) = ((a v b_|_)_|_ v (a v b_|__|_)_|_)
32		oran3 85	. . . . . . . . . . 11 ((a v b_|_)_|_ v (a v b_|__|_)_|_) = ((a v b_|_) ^ (a v b_|__|_))_|_
33	31, 32	ax-r2 35	. . . . . . . . . 10 ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)) = ((a v b_|_) ^ (a v b_|__|_))_|_
34	33	lor 66	. . . . . . . . 9 (((a v b_|_) ^ (a v b_|__|_)) v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))) = (((a v b_|_) ^ (a v b_|__|_)) v ((a v b_|_) ^ (a v b_|__|_))_|_)
35		df-t 40	. . . . . . . . . 10 1 = (((a v b_|_) ^ (a v b_|__|_)) v ((a v b_|_) ^ (a v b_|__|_))_|_)
36	35	ax-r1 34	. . . . . . . . 9 (((a v b_|_) ^ (a v b_|__|_)) v ((a v b_|_) ^ (a v b_|__|_))_|_) = 1
37	34, 36	ax-r2 35	. . . . . . . 8 (((a v b_|_) ^ (a v b_|__|_)) v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))) = 1
38	26, 37	2an 72	. . . . . . 7 ((a_|_ v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))) ^ (((a v b_|_) ^ (a v b_|__|_)) v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)))) = (a_|_ ^ 1)
39		an1 98	. . . . . . 7 (a_|_ ^ 1) = a_|_
40	38, 39	ax-r2 35	. . . . . 6 ((a_|_ v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))) ^ (((a v b_|_) ^ (a v b_|__|_)) v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)))) = a_|_
41	20, 40	ax-r2 35	. . . . 5 ((a_|_ ^ ((a v b_|_) ^ (a v b_|__|_))) v ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))) = a_|_
42	12, 41	ax-r2 35	. . . 4 ((a_|_ ^ (a ->3 b_|_)_|_) v (a_|_ ^ (a ->3 b_|_)_|__|_)) = a_|_
43		comid 179	. . . . . . 7 a C a
44	43	comcom2 175	. . . . . 6 a C a_|_
45		comi31 490	. . . . . . 7 a C (a ->3 b_|_)
46	45	comcom2 175	. . . . . 6 a C (a ->3 b_|_)_|_
47	44, 46	fh1 451	. . . . 5 (a ^ (a_|_ v (a ->3 b_|_)_|_)) = ((a ^ a_|_) v (a ^ (a ->3 b_|_)_|_))
48		dff 93	. . . . . . . 8 0 = (a ^ a_|_)
49	48	ax-r1 34	. . . . . . 7 (a ^ a_|_) = 0
50		ancom 68	. . . . . . . 8 (a ^ (a ->3 b_|_)_|_) = ((a ->3 b_|_)_|_ ^ a)
51		u3lemnaa 624	. . . . . . . 8 ((a ->3 b_|_)_|_ ^ a) = (a ^ b_|__|_)
52	50, 51	ax-r2 35	. . . . . . 7 (a ^ (a ->3 b_|_)_|_) = (a ^ b_|__|_)
53	49, 52	2or 67	. . . . . 6 ((a ^ a_|_) v (a ^ (a ->3 b_|_)_|_)) = (0 v (a ^ b_|__|_))
54		ax-a2 30	. . . . . . 7 (0 v (a ^ b_|__|_)) = ((a ^ b_|__|_) v 0)
55		or0 94	. . . . . . 7 ((a ^ b_|__|_) v 0) = (a ^ b_|__|_)
56	54, 55	ax-r2 35	. . . . . 6 (0 v (a ^ b_|__|_)) = (a ^ b_|__|_)
57	53, 56	ax-r2 35	. . . . 5 ((a ^ a_|_) v (a ^ (a ->3 b_|_)_|_)) = (a ^ b_|__|_)
58	47, 57	ax-r2 35	. . . 4 (a ^ (a_|_ v (a ->3 b_|_)_|_)) = (a ^ b_|__|_)
59	42, 58	2or 67	. . 3 (((a_|_ ^ (a ->3 b_|_)_|_) v (a_|_ ^ (a ->3 b_|_)_|__|_)) v (a ^ (a_|_ v (a ->3 b_|_)_|_))) = (a_|_ v (a ^ b_|__|_))
60		ax-a1 29	. . . . . . 7 b = b_|__|_
61	60	ax-r1 34	. . . . . 6 b_|__|_ = b
62	61	lan 70	. . . . 5 (a ^ b_|__|_) = (a ^ b)
63	62	lor 66	. . . 4 (a_|_ v (a ^ b_|__|_)) = (a_|_ v (a ^ b))
64		df-i1 43	. . . . 5 (a ->1 b) = (a_|_ v (a ^ b))
65	64	ax-r1 34	. . . 4 (a_|_ v (a ^ b)) = (a ->1 b)
66	63, 65	ax-r2 35	. . 3 (a_|_ v (a ^ b_|__|_)) = (a ->1 b)
67	59, 66	ax-r2 35	. 2 (((a_|_ ^ (a ->3 b_|_)_|_) v (a_|_ ^ (a ->3 b_|_)_|__|_)) v (a ^ (a_|_ v (a ->3 b_|_)_|_))) = (a ->1 b)
68	1, 67	ax-r2 35	1 (a ->3 (a ->3 b_|_)_|_) = (a ->1 b)

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7  1wt 9  0wf 10   ->1 wi1 13   ->3 wi3 15

This theorem is referenced by:  u3lem14aa2 775

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i3 45  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org