Theorem u3lem11 768

Description: Lemma for unified implication study.

Assertion

Ref	Expression
u3lem11	(a ->3 (b_|_ ^ (a v b))) = (a ->3 b_|_)

Proof of Theorem u3lem11

Step	Hyp	Ref	Expression
1		df-i3 45	. 2 (a ->3 (b_|_ ^ (a v b))) = (((a_|_ ^ (b_|_ ^ (a v b))) v (a_|_ ^ (b_|_ ^ (a v b))_|_)) v (a ^ (a_|_ v (b_|_ ^ (a v b)))))
2		ax-a1 29	. . . . . 6 b = b_|__|_
3	2	lan 70	. . . . 5 (a_|_ ^ b) = (a_|_ ^ b_|__|_)
4	3	lor 66	. . . 4 ((a_|_ ^ b_|_) v (a_|_ ^ b)) = ((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_))
5	4	ax-r5 37	. . 3 (((a_|_ ^ b_|_) v (a_|_ ^ b)) v (a ^ (a_|_ v b_|_))) = (((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)) v (a ^ (a_|_ v b_|_)))
6		oran 79	. . . . . . . 8 (a v b) = (a_|_ ^ b_|_)_|_
7	6	lan 70	. . . . . . 7 ((a_|_ ^ b_|_) ^ (a v b)) = ((a_|_ ^ b_|_) ^ (a_|_ ^ b_|_)_|_)
8		anass 69	. . . . . . . 8 ((a_|_ ^ b_|_) ^ (a v b)) = (a_|_ ^ (b_|_ ^ (a v b)))
9	8	ax-r1 34	. . . . . . 7 (a_|_ ^ (b_|_ ^ (a v b))) = ((a_|_ ^ b_|_) ^ (a v b))
10		dff 93	. . . . . . 7 0 = ((a_|_ ^ b_|_) ^ (a_|_ ^ b_|_)_|_)
11	7, 9, 10	3tr1 60	. . . . . 6 (a_|_ ^ (b_|_ ^ (a v b))) = 0
12		anor3 82	. . . . . . . . . . . 12 (a_|_ ^ b_|_) = (a v b)_|_
13	12	ax-r5 37	. . . . . . . . . . 11 ((a_|_ ^ b_|_) v b) = ((a v b)_|_ v b)
14		ax-a2 30	. . . . . . . . . . 11 ((a v b)_|_ v b) = (b v (a v b)_|_)
15	13, 14	ax-r2 35	. . . . . . . . . 10 ((a_|_ ^ b_|_) v b) = (b v (a v b)_|_)
16		oran1 83	. . . . . . . . . 10 (b v (a v b)_|_) = (b_|_ ^ (a v b))_|_
17	15, 16	ax-r2 35	. . . . . . . . 9 ((a_|_ ^ b_|_) v b) = (b_|_ ^ (a v b))_|_
18	17	ax-r1 34	. . . . . . . 8 (b_|_ ^ (a v b))_|_ = ((a_|_ ^ b_|_) v b)
19	18	lan 70	. . . . . . 7 (a_|_ ^ (b_|_ ^ (a v b))_|_) = (a_|_ ^ ((a_|_ ^ b_|_) v b))
20		coman1 177	. . . . . . . . 9 (a_|_ ^ b_|_) C a_|_
21		coman2 178	. . . . . . . . . 10 (a_|_ ^ b_|_) C b_|_
22	21	comcom7 442	. . . . . . . . 9 (a_|_ ^ b_|_) C b
23	20, 22	fh2 452	. . . . . . . 8 (a_|_ ^ ((a_|_ ^ b_|_) v b)) = ((a_|_ ^ (a_|_ ^ b_|_)) v (a_|_ ^ b))
24		anass 69	. . . . . . . . . . 11 ((a_|_ ^ a_|_) ^ b_|_) = (a_|_ ^ (a_|_ ^ b_|_))
25	24	ax-r1 34	. . . . . . . . . 10 (a_|_ ^ (a_|_ ^ b_|_)) = ((a_|_ ^ a_|_) ^ b_|_)
26		anidm 103	. . . . . . . . . . 11 (a_|_ ^ a_|_) = a_|_
27	26	ran 71	. . . . . . . . . 10 ((a_|_ ^ a_|_) ^ b_|_) = (a_|_ ^ b_|_)
28	25, 27	ax-r2 35	. . . . . . . . 9 (a_|_ ^ (a_|_ ^ b_|_)) = (a_|_ ^ b_|_)
29	28	ax-r5 37	. . . . . . . 8 ((a_|_ ^ (a_|_ ^ b_|_)) v (a_|_ ^ b)) = ((a_|_ ^ b_|_) v (a_|_ ^ b))
30	23, 29	ax-r2 35	. . . . . . 7 (a_|_ ^ ((a_|_ ^ b_|_) v b)) = ((a_|_ ^ b_|_) v (a_|_ ^ b))
31	19, 30	ax-r2 35	. . . . . 6 (a_|_ ^ (b_|_ ^ (a v b))_|_) = ((a_|_ ^ b_|_) v (a_|_ ^ b))
32	11, 31	2or 67	. . . . 5 ((a_|_ ^ (b_|_ ^ (a v b))) v (a_|_ ^ (b_|_ ^ (a v b))_|_)) = (0 v ((a_|_ ^ b_|_) v (a_|_ ^ b)))
33		ax-a2 30	. . . . . 6 (0 v ((a_|_ ^ b_|_) v (a_|_ ^ b))) = (((a_|_ ^ b_|_) v (a_|_ ^ b)) v 0)
34		or0 94	. . . . . 6 (((a_|_ ^ b_|_) v (a_|_ ^ b)) v 0) = ((a_|_ ^ b_|_) v (a_|_ ^ b))
35	33, 34	ax-r2 35	. . . . 5 (0 v ((a_|_ ^ b_|_) v (a_|_ ^ b))) = ((a_|_ ^ b_|_) v (a_|_ ^ b))
36	32, 35	ax-r2 35	. . . 4 ((a_|_ ^ (b_|_ ^ (a v b))) v (a_|_ ^ (b_|_ ^ (a v b))_|_)) = ((a_|_ ^ b_|_) v (a_|_ ^ b))
37		ax-a2 30	. . . . . . . . . . 11 (a_|_ v a) = (a v a_|_)
38		df-t 40	. . . . . . . . . . . 12 1 = (a v a_|_)
39	38	ax-r1 34	. . . . . . . . . . 11 (a v a_|_) = 1
40	37, 39	ax-r2 35	. . . . . . . . . 10 (a_|_ v a) = 1
41	40	ax-r5 37	. . . . . . . . 9 ((a_|_ v a) v b) = (1 v b)
42		ax-a3 31	. . . . . . . . 9 ((a_|_ v a) v b) = (a_|_ v (a v b))
43		ax-a2 30	. . . . . . . . . 10 (1 v b) = (b v 1)
44		or1 96	. . . . . . . . . 10 (b v 1) = 1
45	43, 44	ax-r2 35	. . . . . . . . 9 (1 v b) = 1
46	41, 42, 45	3tr2 61	. . . . . . . 8 (a_|_ v (a v b)) = 1
47	46	ran 71	. . . . . . 7 ((a_|_ v (a v b)) ^ (a_|_ v b_|_)) = (1 ^ (a_|_ v b_|_))
48		ancom 68	. . . . . . . 8 (1 ^ (a_|_ v b_|_)) = ((a_|_ v b_|_) ^ 1)
49		an1 98	. . . . . . . 8 ((a_|_ v b_|_) ^ 1) = (a_|_ v b_|_)
50	48, 49	ax-r2 35	. . . . . . 7 (1 ^ (a_|_ v b_|_)) = (a_|_ v b_|_)
51	47, 50	ax-r2 35	. . . . . 6 ((a_|_ v (a v b)) ^ (a_|_ v b_|_)) = (a_|_ v b_|_)
52	51	lan 70	. . . . 5 (a ^ ((a_|_ v (a v b)) ^ (a_|_ v b_|_))) = (a ^ (a_|_ v b_|_))
53		ancom 68	. . . . . . . 8 (b_|_ ^ (a v b)) = ((a v b) ^ b_|_)
54	53	lor 66	. . . . . . 7 (a_|_ v (b_|_ ^ (a v b))) = (a_|_ v ((a v b) ^ b_|_))
55		comor1 443	. . . . . . . . 9 (a v b) C a
56	55	comcom2 175	. . . . . . . 8 (a v b) C a_|_
57		comor2 444	. . . . . . . . 9 (a v b) C b
58	57	comcom2 175	. . . . . . . 8 (a v b) C b_|_
59	56, 58	fh4 454	. . . . . . 7 (a_|_ v ((a v b) ^ b_|_)) = ((a_|_ v (a v b)) ^ (a_|_ v b_|_))
60	54, 59	ax-r2 35	. . . . . 6 (a_|_ v (b_|_ ^ (a v b))) = ((a_|_ v (a v b)) ^ (a_|_ v b_|_))
61	60	lan 70	. . . . 5 (a ^ (a_|_ v (b_|_ ^ (a v b)))) = (a ^ ((a_|_ v (a v b)) ^ (a_|_ v b_|_)))
62		id 58	. . . . 5 (a ^ (a_|_ v b_|_)) = (a ^ (a_|_ v b_|_))
63	52, 61, 62	3tr1 60	. . . 4 (a ^ (a_|_ v (b_|_ ^ (a v b)))) = (a ^ (a_|_ v b_|_))
64	36, 63	2or 67	. . 3 (((a_|_ ^ (b_|_ ^ (a v b))) v (a_|_ ^ (b_|_ ^ (a v b))_|_)) v (a ^ (a_|_ v (b_|_ ^ (a v b))))) = (((a_|_ ^ b_|_) v (a_|_ ^ b)) v (a ^ (a_|_ v b_|_)))
65		df-i3 45	. . 3 (a ->3 b_|_) = (((a_|_ ^ b_|_) v (a_|_ ^ b_|__|_)) v (a ^ (a_|_ v b_|_)))
66	5, 64, 65	3tr1 60	. 2 (((a_|_ ^ (b_|_ ^ (a v b))) v (a_|_ ^ (b_|_ ^ (a v b))_|_)) v (a ^ (a_|_ v (b_|_ ^ (a v b))))) = (a ->3 b_|_)
67	1, 66	ax-r2 35	1 (a ->3 (b_|_ ^ (a v b))) = (a ->3 b_|_)

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

This theorem is referenced by:  u3lem11a 769

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-i3 45  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org