Theorem oa6fromdualn 934

Description: Dual to conventional 6-variable OA law.

Hypothesis

Ref	Expression
oa6fromdualn.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
oa6fromdualn	(((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 oa6fromdualn

Step	Hyp	Ref	Expression
1		oa6fromdualn.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		ax-a1 29	. . . 4 b = b_|__|_
3		ax-a1 29	. . . . 5 a = a_|__|_
4		ax-a1 29	. . . . . 6 c = c_|__|_
5	3, 4	2an 72	. . . . . . . 8 (a ^ c) = (a_|__|_ ^ c_|__|_)
6		ax-a1 29	. . . . . . . . 9 d = d_|__|_
7	2, 6	2an 72	. . . . . . . 8 (b ^ d) = (b_|__|_ ^ d_|__|_)
8	5, 7	2or 67	. . . . . . 7 ((a ^ c) v (b ^ d)) = ((a_|__|_ ^ c_|__|_) v (b_|__|_ ^ d_|__|_))
9		ax-a1 29	. . . . . . . . . 10 e = e_|__|_
10	3, 9	2an 72	. . . . . . . . 9 (a ^ e) = (a_|__|_ ^ e_|__|_)
11		ax-a1 29	. . . . . . . . . 10 f = f_|__|_
12	2, 11	2an 72	. . . . . . . . 9 (b ^ f) = (b_|__|_ ^ f_|__|_)
13	10, 12	2or 67	. . . . . . . 8 ((a ^ e) v (b ^ f)) = ((a_|__|_ ^ e_|__|_) v (b_|__|_ ^ f_|__|_))
14	4, 9	2an 72	. . . . . . . . 9 (c ^ e) = (c_|__|_ ^ e_|__|_)
15	6, 11	2an 72	. . . . . . . . 9 (d ^ f) = (d_|__|_ ^ f_|__|_)
16	14, 15	2or 67	. . . . . . . 8 ((c ^ e) v (d ^ f)) = ((c_|__|_ ^ e_|__|_) v (d_|__|_ ^ f_|__|_))
17	13, 16	2an 72	. . . . . . 7 (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f))) = (((a_|__|_ ^ e_|__|_) v (b_|__|_ ^ f_|__|_)) ^ ((c_|__|_ ^ e_|__|_) v (d_|__|_ ^ f_|__|_)))
18	8, 17	2or 67	. . . . . 6 (((a ^ c) v (b ^ d)) v (((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_|__|_))))
19	4, 18	2an 72	. . . . 5 (c ^ (((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_|__|_)))))
20	3, 19	2or 67	. . . 4 (a v (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f)))))) = (a_|__|_ v (c_|__|_ ^ (((a_|__|_ ^ c_|__|_) v (b_|__|_ ^ d_|__|_)) v (((a_|__|_ ^ e_|__|_) v (b_|__|_ ^ f_|__|_)) ^ ((c_|__|_ ^ e_|__|_) v (d_|__|_ ^ f_|__|_))))))
21	2, 20	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_|__|_ v (c_|__|_ ^ (((a_|__|_ ^ c_|__|_) v (b_|__|_ ^ d_|__|_)) v (((a_|__|_ ^ e_|__|_) v (b_|__|_ ^ f_|__|_)) ^ ((c_|__|_ ^ e_|__|_) v (d_|__|_ ^ f_|__|_)))))))
22	3, 2	2an 72	. . . . 5 (a ^ b) = (a_|__|_ ^ b_|__|_)
23	4, 6	2an 72	. . . . 5 (c ^ d) = (c_|__|_ ^ d_|__|_)
24	22, 23	2or 67	. . . 4 ((a ^ b) v (c ^ d)) = ((a_|__|_ ^ b_|__|_) v (c_|__|_ ^ d_|__|_))
25	9, 11	2an 72	. . . 4 (e ^ f) = (e_|__|_ ^ f_|__|_)
26	24, 25	2or 67	. . 3 (((a ^ b) v (c ^ d)) v (e ^ f)) = (((a_|__|_ ^ b_|__|_) v (c_|__|_ ^ d_|__|_)) v (e_|__|_ ^ f_|__|_))
27	1, 21, 26	le3tr2 133	. 2 (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_|__|_))
28	27	oa6fromdual 933	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_|_)))))))

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-le1 122  df-le2 123

metamath.org