Theorem oa8todual 971

Description: Conventional to dual 8-variable OA law.

Hypothesis

Ref	Expression
oa8to5.1	(((a' v b') ^ (c' v d')) ^ ((e' v f') ^ (g' v h'))) =< (b' v (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))))

Assertion

Ref	Expression
oa8todual	(b ^ (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))))) =< (((a ^ b) v (c ^ d)) v ((e ^ f) v (g ^ h)))

Proof of Theorem oa8todual

Step	Hyp	Ref	Expression
1		oa8to5.1	. . 3 (((a' v b') ^ (c' v d')) ^ ((e' v f') ^ (g' v h'))) =< (b' v (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))))
2	1	lecon 154	. 2 (b' v (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))))' =< (((a' v b') ^ (c' v d')) ^ ((e' v f') ^ (g' v h')))'
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	. . . . . . . . . . . . . 14 (a ^ c) = (a' v c')'
7		df-a 40	. . . . . . . . . . . . . 14 (b ^ d) = (b' v d')'
8	6, 7	2or 72	. . . . . . . . . . . . 13 ((a ^ c) v (b ^ d)) = ((a' v c')' v (b' v d')')
9		oran3 93	. . . . . . . . . . . . 13 ((a' v c')' v (b' v d')') = ((a' v c') ^ (b' v d'))'
10	8, 9	ax-r2 36	. . . . . . . . . . . 12 ((a ^ c) v (b ^ d)) = ((a' v c') ^ (b' v d'))'
11		df-a 40	. . . . . . . . . . . . . . . 16 (a ^ g) = (a' v g')'
12		df-a 40	. . . . . . . . . . . . . . . 16 (b ^ h) = (b' v h')'
13	11, 12	2or 72	. . . . . . . . . . . . . . 15 ((a ^ g) v (b ^ h)) = ((a' v g')' v (b' v h')')
14		oran3 93	. . . . . . . . . . . . . . 15 ((a' v g')' v (b' v h')') = ((a' v g') ^ (b' v h'))'
15	13, 14	ax-r2 36	. . . . . . . . . . . . . 14 ((a ^ g) v (b ^ h)) = ((a' v g') ^ (b' v h'))'
16		df-a 40	. . . . . . . . . . . . . . . 16 (c ^ g) = (c' v g')'
17		df-a 40	. . . . . . . . . . . . . . . 16 (d ^ h) = (d' v h')'
18	16, 17	2or 72	. . . . . . . . . . . . . . 15 ((c ^ g) v (d ^ h)) = ((c' v g')' v (d' v h')')
19		oran3 93	. . . . . . . . . . . . . . 15 ((c' v g')' v (d' v h')') = ((c' v g') ^ (d' v h'))'
20	18, 19	ax-r2 36	. . . . . . . . . . . . . 14 ((c ^ g) v (d ^ h)) = ((c' v g') ^ (d' v h'))'
21	15, 20	2an 79	. . . . . . . . . . . . 13 (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h))) = (((a' v g') ^ (b' v h'))' ^ ((c' v g') ^ (d' v h'))')
22		anor3 90	. . . . . . . . . . . . 13 (((a' v g') ^ (b' v h'))' ^ ((c' v g') ^ (d' v h'))') = (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))'
23	21, 22	ax-r2 36	. . . . . . . . . . . 12 (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h))) = (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))'
24	10, 23	2or 72	. . . . . . . . . . 11 (((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) = (((a' v c') ^ (b' v d'))' v (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))')
25		oran3 93	. . . . . . . . . . 11 (((a' v c') ^ (b' v d'))' v (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))') = (((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h'))))'
26	24, 25	ax-r2 36	. . . . . . . . . 10 (((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) = (((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h'))))'
27		df-a 40	. . . . . . . . . . . . . . . 16 (a ^ e) = (a' v e')'
28		df-a 40	. . . . . . . . . . . . . . . 16 (b ^ f) = (b' v f')'
29	27, 28	2or 72	. . . . . . . . . . . . . . 15 ((a ^ e) v (b ^ f)) = ((a' v e')' v (b' v f')')
30		oran3 93	. . . . . . . . . . . . . . 15 ((a' v e')' v (b' v f')') = ((a' v e') ^ (b' v f'))'
31	29, 30	ax-r2 36	. . . . . . . . . . . . . 14 ((a ^ e) v (b ^ f)) = ((a' v e') ^ (b' v f'))'
32		df-a 40	. . . . . . . . . . . . . . . . . 18 (e ^ g) = (e' v g')'
33		df-a 40	. . . . . . . . . . . . . . . . . 18 (f ^ h) = (f' v h')'
34	32, 33	2or 72	. . . . . . . . . . . . . . . . 17 ((e ^ g) v (f ^ h)) = ((e' v g')' v (f' v h')')
35		oran3 93	. . . . . . . . . . . . . . . . 17 ((e' v g')' v (f' v h')') = ((e' v g') ^ (f' v h'))'
36	34, 35	ax-r2 36	. . . . . . . . . . . . . . . 16 ((e ^ g) v (f ^ h)) = ((e' v g') ^ (f' v h'))'
37	15, 36	2an 79	. . . . . . . . . . . . . . 15 (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h))) = (((a' v g') ^ (b' v h'))' ^ ((e' v