Theorem oa6todual 952

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 154	. 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 30	. . . 4 b = b''
4		ax-a1 30	. . . . . 6 a = a''
5		ax-a1 30	. . . . . . . 8 c = c''
6		df-a 40	. . . . . . . . . . . 12 (a ^ c) = (a' v c')'
7		df-a 40	. . . . . . . . . . . 12 (b ^ d) = (b' v d')'
8	6, 7	2or 72	. . . . . . . . . . 11 ((a ^ c) v (b ^ d)) = ((a' v c')' v (b' v d')')
9		oran3 93	. . . . . . . . . . 11 ((a' v c')' v (b' v d')') = ((a' v c') ^ (b' v d'))'
10	8, 9	ax-r2 36	. . . . . . . . . 10 ((a ^ c) v (b ^ d)) = ((a' v c') ^ (b' v d'))'
11		df-a 40	. . . . . . . . . . . . . 14 (a ^ e) = (a' v e')'
12		df-a 40	. . . . . . . . . . . . . 14 (b ^ f) = (b' v f')'
13	11, 12	2or 72	. . . . . . . . . . . . 13 ((a ^ e) v (b ^ f)) = ((a' v e')' v (b' v f')')
14		oran3 93	. . . . . . . . . . . . 13 ((a' v e')' v (b' v f')') = ((a' v e') ^ (b' v f'))'
15	13, 14	ax-r2 36	. . . . . . . . . . . 12 ((a ^ e) v (b ^ f)) = ((a' v e') ^ (b' v f'))'
16		df-a 40	. . . . . . . . . . . . . 14 (c ^ e) = (c' v e')'
17		df-a 40	. . . . . . . . . . . . . 14 (d ^ f) = (d' v f')'
18	16, 17	2or 72	. . . . . . . . . . . . 13 ((c ^ e) v (d ^ f)) = ((c' v e')' v (d' v f')')
19		oran3 93	. . . . . . . . . . . . 13 ((c' v e')' v (d' v f')') = ((c' v e') ^ (d' v f'))'
20	18, 19	ax-r2 36	. . . . . . . . . . . 12 ((c ^ e) v (d ^ f)) = ((c' v e') ^ (d' v f'))'
21	15, 20	2an 79	. . . . . . . . . . 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 90	. . . . . . . . . . 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 36	. . . . . . . . . 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 72	. . . . . . . . 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 93	. . . . . . . . 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 36	. . . . . . . 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 79	. . . . . . 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 90	. . . . . . 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 36	. . . . . 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 72	. . . . 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 93	. . . . 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 36	. . . 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 79	. . 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