Theorem 2oalem1 807

Description: Lemma for OA-like stuff with ->2 instead of ->0.

Assertion

Ref	Expression
2oalem1	((a ->2 b)_|_ v ((b v c) v ((a ->2 b) ^ (a ->2 c)))) = 1

Proof of Theorem 2oalem1

Step	Hyp	Ref	Expression
1		or12 73	. 2 ((a ->2 b)_|_ v ((b v c) v ((a ->2 b) ^ (a ->2 c)))) = ((b v c) v ((a ->2 b)_|_ v ((a ->2 b) ^ (a ->2 c))))
2		ud2lem0c 270	. . . 4 (a ->2 b)_|_ = (b_|_ ^ (a v b))
3		df-i2 44	. . . . 5 (a ->2 b) = (b v (a_|_ ^ b_|_))
4		df-i2 44	. . . . 5 (a ->2 c) = (c v (a_|_ ^ c_|_))
5	3, 4	2an 72	. . . 4 ((a ->2 b) ^ (a ->2 c)) = ((b v (a_|_ ^ b_|_)) ^ (c v (a_|_ ^ c_|_)))
6	2, 5	2or 67	. . 3 ((a ->2 b)_|_ v ((a ->2 b) ^ (a ->2 c))) = ((b_|_ ^ (a v b)) v ((b v (a_|_ ^ b_|_)) ^ (c v (a_|_ ^ c_|_))))
7	6	lor 66	. 2 ((b v c) v ((a ->2 b)_|_ v ((a ->2 b) ^ (a ->2 c)))) = ((b v c) v ((b_|_ ^ (a v b)) v ((b v (a_|_ ^ b_|_)) ^ (c v (a_|_ ^ c_|_)))))
8		or32 75	. . . . 5 ((b v c) v (b_|_ ^ (a v b))) = ((b v (b_|_ ^ (a v b))) v c)
9		oml 427	. . . . . . 7 (b v (b_|_ ^ (b v a))) = (b v a)
10		ax-a2 30	. . . . . . . . 9 (a v b) = (b v a)
11	10	lan 70	. . . . . . . 8 (b_|_ ^ (a v b)) = (b_|_ ^ (b v a))
12	11	lor 66	. . . . . . 7 (b v (b_|_ ^ (a v b))) = (b v (b_|_ ^ (b v a)))
13	9, 12, 10	3tr1 60	. . . . . 6 (b v (b_|_ ^ (a v b))) = (a v b)
14	13	ax-r5 37	. . . . 5 ((b v (b_|_ ^ (a v b))) v c) = ((a v b) v c)
15	8, 14	ax-r2 35	. . . 4 ((b v c) v (b_|_ ^ (a v b))) = ((a v b) v c)
16	15	ax-r5 37	. . 3 (((b v c) v (b_|_ ^ (a v b))) v ((b v (a_|_ ^ b_|_)) ^ (c v (a_|_ ^ c_|_)))) = (((a v b) v c) v ((b v (a_|_ ^ b_|_)) ^ (c v (a_|_ ^ c_|_))))
17		ax-a3 31	. . 3 (((b v c) v (b_|_ ^ (a v b))) v ((b v (a_|_ ^ b_|_)) ^ (c v (a_|_ ^ c_|_)))) = ((b v c) v ((b_|_ ^ (a v b)) v ((b v (a_|_ ^ b_|_)) ^ (c v (a_|_ ^ c_|_)))))
18		oran 79	. . . . . . . . . . . . 13 (a v b) = (a_|_ ^ b_|_)_|_
19	18	lan 70	. . . . . . . . . . . 12 (b_|_ ^ (a v b)) = (b_|_ ^ (a_|_ ^ b_|_)_|_)
20		anor3 82	. . . . . . . . . . . 12 (b_|_ ^ (a_|_ ^ b_|_)_|_) = (b v (a_|_ ^ b_|_))_|_
21	19, 20	ax-r2 35	. . . . . . . . . . 11 (b_|_ ^ (a v b)) = (b v (a_|_ ^ b_|_))_|_
22	21	ax-r1 34	. . . . . . . . . 10 (b v (a_|_ ^ b_|_))_|_ = (b_|_ ^ (a v b))
23		lear 153	. . . . . . . . . 10 (b_|_ ^ (a v b)) =< (a v b)
24	22, 23	bltr 130	. . . . . . . . 9 (b v (a_|_ ^ b_|_))_|_ =< (a v b)
25		leo 150	. . . . . . . . 9 (a v b) =< ((a v b) v c)
26	24, 25	letr 129	. . . . . . . 8 (b v (a_|_ ^ b_|_))_|_ =< ((a v b) v c)
27	26	lecom 172	. . . . . . 7 (b v (a_|_ ^ b_|_))_|_ C ((a v b) v c)
28	27	comcom6 441	. . . . . 6 (b v (a_|_ ^ b_|_)) C ((a v b) v c)
29	28	comcom 435	. . . . 5 ((a v b) v c) C (b v (a_|_ ^ b_|_))
30		lear 153	. . . . . . . . . 10 (c_|_ ^ (a v c)) =< (a v c)
31		leo 150	. . . . . . . . . 10 (a v c) =< ((a v c) v b)
32	30, 31	letr 129	. . . . . . . . 9 (c_|_ ^ (a v c)) =< ((a v c) v b)
33		oran 79	. . . . . . . . . . 11 (a v c) = (a_|_ ^ c_|_)_|_
34	33	lan 70	. . . . . . . . . 10 (c_|_ ^ (a v c)) = (c_|_ ^ (a_|_ ^ c_|_)_|_)
35		anor3 82	. . . . . . . . . 10 (c_|_ ^ (a_|_ ^ c_|_)_|_) = (c v (a_|_ ^ c_|_))_|_
36	34, 35	ax-r2 35	. . . . . . . . 9 (c_|_ ^ (a v c)) = (c v (a_|_ ^ c_|_))_|_
37		or32 75	. . . . . . . . 9 ((a v c) v b) = ((a v b) v c)
38	32, 36, 37	le3tr2 133	. . . . . . . 8 (c v (a_|_ ^ c_|_))_|_ =< ((a v b) v c)
39	38	lecom 172	. . . . . . 7 (c v (a_|_ ^ c_|_))_|_ C ((a v b) v c)
40	39	comcom6 441	. . . . . 6 (c v (a_|_ ^ c_|_)) C ((a v b) v c)
41	40	comcom 435	. . . . 5 ((a v b) v c) C (c v (a_|_ ^ c_|_))
42	29, 41	fh3 453	. . . 4 (((a v b) v c) v ((b v (a_|_ ^ b_|_)) ^ (c v (a_|_ ^ c_|_)))) = ((((a v b) v c) v (b v (a_|_ ^ b_|_))) ^ (((a v b) v c) v (c v (a_|_ ^ c_|_))))
43		or12 73	. . . . . 6 (((a v b) v c) v (b v (a_|_ ^ b_|_))) = (b v (((a v b) v c) v (a_|_ ^ b_|_)))
44		or32 75	. . . . . . . 8 (((a v b) v c) v (a_|_ ^ b_|_)) = (((a v b) v (a_|_ ^ b_|_)) v c)
45		ax-a2 30	. . . . . . . 8 (((a v b) v (a_|_ ^ b_|_)) v c) = (c v ((a v b) v (a_|_ ^ b_|_)))
46		anor3 82	. . . . . . . . . . . 12 (a_|_ ^ b_|_) = (a v b)_|_
47	46	lor 66	. . . . . . . . . . 11 ((a v b) v (a_|_ ^ b_|_)) = ((a v b) v (a v b)_|_)
48		df-t 40	. . . . . . . . . . . 12 1 = ((a v b) v (a v b)_|_)
49	48	ax-r1 34	. . . . . . . . . . 11 ((a v b) v (a v b)_|_) = 1
50	47, 49	ax-r2 35	. . . . . . . . . 10 ((a v b) v (a_|_ ^ b_|_)) = 1
51	50	lor 66	. . . . . . . . 9 (c v ((a v b) v (a_|_ ^ b_|_))) = (c v 1)
52		or1 96	. . . . . . . . 9 (c v 1) = 1
53	51, 52	ax-r2 35	. . . . . . . 8 (c v ((a v b) v (a_|_ ^ b_|_))) = 1
54	44, 45, 53	3tr 62	. . . . . . 7 (((a v b) v c) v (a_|_ ^ b_|_)) = 1
55	54	lor 66	. . . . . 6 (b v (((a v b) v c) v (a_|_ ^ b_|_))) = (b v 1)
56		or1 96	. . . . . 6 (b v 1) = 1
57	43, 55, 56	3tr 62	. . . . 5 (((a v b) v c) v (b v (a_|_ ^ b_|_))) = 1
58		or12 73	. . . . . 6 (((a v b) v c) v (c v (a_|_ ^ c_|_))) = (c v (((a v b) v c) v (a_|_ ^ c_|_)))
59		or32 75	. . . . . . . . . 10 ((a v b) v c) = ((a v c) v b)
60		ax-a2 30	. . . . . . . . . 10 ((a v c) v b) = (b v (a v c))
61	59, 60	ax-r2 35	. . . . . . . . 9 ((a v b) v c) = (b v (a v c))
62	61	ax-r5 37	. . . . . . . 8 (((a v b) v c) v (a_|_ ^ c_|_)) = ((b v (a v c)) v (a_|_ ^ c_|_))
63		ax-a3 31	. . . . . . . 8 ((b v (a v c)) v (a_|_ ^ c_|_)) = (b v ((a v c) v (a_|_ ^ c_|_)))
64		anor3 82	. . . . . . . . . . . 12 (a_|_ ^ c_|_) = (a v c)_|_
65	64	lor 66	. . . . . . . . . . 11 ((a v c) v (a_|_ ^ c_|_)) = ((a v c) v (a v c)_|_)
66		df-t 40	. . . . . . . . . . . 12 1 = ((a v c) v (a v c)_|_)
67	66	ax-r1 34	. . . . . . . . . . 11 ((a v c) v (a v c)_|_) = 1
68	65, 67	ax-r2 35	. . . . . . . . . 10 ((a v c) v (a_|_ ^ c_|_)) = 1
69	68	lor 66	. . . . . . . . 9 (b v ((a v c) v (a_|_ ^ c_|_))) = (b v 1)
70	69, 56	ax-r2 35	. . . . . . . 8 (b v ((a v c) v (a_|_ ^ c_|_))) = 1
71	62, 63, 70	3tr 62	. . . . . . 7 (((a v b) v c) v (a_|_ ^ c_|_)) = 1
72	71	lor 66	. . . . . 6 (c v (((a v b) v c) v (a_|_ ^ c_|_))) = (c v 1)
73	58, 72, 52	3tr 62	. . . . 5 (((a v b) v c) v (c v (a_|_ ^ c_|_))) = 1
74	57, 73	2an 72	. . . 4 ((((a v b) v c) v (b v (a_|_ ^ b_|_))) ^ (((a v b) v c) v (c v (a_|_ ^ c