Theorem oa6fromdual 933

Description: Dual to conventional 6-variable OA law.

Hypothesis

Ref	Expression
oa6fromdual.1	(b_|_ ^ (a_|_ v (c_|_ ^ (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_))))))) =< (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))

Assertion

Ref	Expression
oa6fromdual	(((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))

Proof of Theorem oa6fromdual

Step	Hyp	Ref	Expression
1		oa6fromdual.1	. . 3 (b_|_ ^ (a_|_ v (c_|_ ^ (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_))))))) =< (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))
2	1	lecon 146	. 2 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))_|_ =< (b_|_ ^ (a_|_ v (c_|_ ^ (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_)))))))_|_
3		oran 79	. . . . . 6 (a v b) = (a_|_ ^ b_|_)_|_
4		oran 79	. . . . . 6 (c v d) = (c_|_ ^ d_|_)_|_
5	3, 4	2an 72	. . . . 5 ((a v b) ^ (c v d)) = ((a_|_ ^ b_|_)_|_ ^ (c_|_ ^ d_|_)_|_)
6		anor3 82	. . . . 5 ((a_|_ ^ b_|_)_|_ ^ (c_|_ ^ d_|_)_|_) = ((a_|_ ^ b_|_) v (c_|_ ^ d_|_))_|_
7	5, 6	ax-r2 35	. . . 4 ((a v b) ^ (c v d)) = ((a_|_ ^ b_|_) v (c_|_ ^ d_|_))_|_
8		oran 79	. . . 4 (e v f) = (e_|_ ^ f_|_)_|_
9	7, 8	2an 72	. . 3 (((a v b) ^ (c v d)) ^ (e v f)) = (((a_|_ ^ b_|_) v (c_|_ ^ d_|_))_|_ ^ (e_|_ ^ f_|_)_|_)
10		anor3 82	. . 3 (((a_|_ ^ b_|_) v (c_|_ ^ d_|_))_|_ ^ (e_|_ ^ f_|_)_|_) = (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))_|_
11	9, 10	ax-r2 35	. 2 (((a v b) ^ (c v d)) ^ (e v f)) = (((a_|_ ^ b_|_) v (c_|_ ^ d_|_)) v (e_|_ ^ f_|_))_|_
12		ax-a1 29	. . . 4 b = b_|__|_
13		ax-a1 29	. . . . . 6 a = a_|__|_
14		ax-a1 29	. . . . . . . 8 c = c_|__|_
15		oran 79	. . . . . . . . . . . 12 (a v c) = (a_|_ ^ c_|_)_|_
16		oran 79	. . . . . . . . . . . 12 (b v d) = (b_|_ ^ d_|_)_|_
17	15, 16	2an 72	. . . . . . . . . . 11 ((a v c) ^ (b v d)) = ((a_|_ ^ c_|_)_|_ ^ (b_|_ ^ d_|_)_|_)
18		anor3 82	. . . . . . . . . . 11 ((a_|_ ^ c_|_)_|_ ^ (b_|_ ^ d_|_)_|_) = ((a_|_ ^ c_|_) v (b_|_ ^ d_|_))_|_
19	17, 18	ax-r2 35	. . . . . . . . . 10 ((a v c) ^ (b v d)) = ((a_|_ ^ c_|_) v (b_|_ ^ d_|_))_|_
20		oran 79	. . . . . . . . . . . . . 14 (a v e) = (a_|_ ^ e_|_)_|_
21		oran 79	. . . . . . . . . . . . . 14 (b v f) = (b_|_ ^ f_|_)_|_
22	20, 21	2an 72	. . . . . . . . . . . . 13 ((a v e) ^ (b v f)) = ((a_|_ ^ e_|_)_|_ ^ (b_|_ ^ f_|_)_|_)
23		anor3 82	. . . . . . . . . . . . 13 ((a_|_ ^ e_|_)_|_ ^ (b_|_ ^ f_|_)_|_) = ((a_|_ ^ e_|_) v (b_|_ ^ f_|_))_|_
24	22, 23	ax-r2 35	. . . . . . . . . . . 12 ((a v e) ^ (b v f)) = ((a_|_ ^ e_|_) v (b_|_ ^ f_|_))_|_
25		oran 79	. . . . . . . . . . . . . 14 (c v e) = (c_|_ ^ e_|_)_|_
26		oran 79	. . . . . . . . . . . . . 14 (d v f) = (d_|_ ^ f_|_)_|_
27	25, 26	2an 72	. . . . . . . . . . . . 13 ((c v e) ^ (d v f)) = ((c_|_ ^ e_|_)_|_ ^ (d_|_ ^ f_|_)_|_)
28		anor3 82	. . . . . . . . . . . . 13 ((c_|_ ^ e_|_)_|_ ^ (d_|_ ^ f_|_)_|_) = ((c_|_ ^ e_|_) v (d_|_ ^ f_|_))_|_
29	27, 28	ax-r2 35	. . . . . . . . . . . 12 ((c v e) ^ (d v f)) = ((c_|_ ^ e_|_) v (d_|_ ^ f_|_))_|_
30	24, 29	2or 67	. . . . . . . . . . 11 (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))) = (((a_|_ ^ e_|_) v (b_|_ ^ f_|_))_|_ v ((c_|_ ^ e_|_) v (d_|_ ^ f_|_))_|_)
31		oran3 85	. . . . . . . . . . 11 (((a_|_ ^ e_|_) v (b_|_ ^ f_|_))_|_ v ((c_|_ ^ e_|_) v (d_|_ ^ f_|_))_|_) = (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_)))_|_
32	30, 31	ax-r2 35	. . . . . . . . . 10 (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))) = (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_)))_|_
33	19, 32	2an 72	. . . . . . . . 9 (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))) = (((a_|_ ^ c_|_) v (b_|_ ^ d_|_))_|_ ^ (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_)))_|_)
34		anor3 82	. . . . . . . . 9 (((a_|_ ^ c_|_) v (b_|_ ^ d_|_))_|_ ^ (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_)))_|_) = (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_))))_|_
35	33, 34	ax-r2 35	. . . . . . . 8 (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))) = (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_))))_|_
36	14, 35	2or 67	. . . . . . 7 (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))))) = (c_|__|_ v (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_))))_|_)
37		oran3 85	. . . . . . 7 (c_|__|_ v (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_))))_|_) = (c_|_ ^ (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_)))))_|_
38	36, 37	ax-r2 35	. . . . . 6 (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))))) = (c_|_ ^ (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_)))))_|_
39	13, 38	2an 72	. . . . 5 (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))) = (a_|__|_ ^ (c_|_ ^ (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (b_|_ ^ f_|_)) ^ ((c_|_ ^ e_|_) v (d_|_ ^ f_|_)))))_|_)
40		anor3 82	. . . . 5 (a_|__|_ ^ (c_|_ ^ (((a_|_ ^ c_|_) v (b_|_ ^ d_|_)) v (((a_|_ ^ e_|_) v (