Theorem oa6todual 932

Description: Conventional to dual 6-variable OA law.

Hypothesis

Ref	Expression
oa6todual.1	(((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_|_)))))))

Assertion

Ref	Expression
oa6todual	(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))

Proof of Theorem oa6todual

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