Theorem oa8to5 972

Description: Orthoarguesian law 5OA converted from 8 to 5 variables.

Hypotheses

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')))))))))
oa8to5.2	b' = (a ->1 j)'
oa8to5.3	d' = (c ->1 j)'
oa8to5.4	f' = (e ->1 j)'
oa8to5.5	h' = (g ->1 j)'

Assertion

Ref

Expression

oa8to5

((a ->1 j) ^ (a v (c ^ ((((a ^ c) v ((a ->1 j) ^ (c ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j))))) v ((((a ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))) ^ (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))))))))) =< (((a ^ j) v (c ^ j)) v ((e ^ j) v (g ^ j)))

Proof of Theorem oa8to5

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	oa8todual 971	. 2 (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)))
3		oa8to5.2	. . . 4 b' = (a ->1 j)'
4	3	con1 66	. . 3 b = (a ->1 j)
5		oa8to5.3	. . . . . . . . . 10 d' = (c ->1 j)'
6	5	con1 66	. . . . . . . . 9 d = (c ->1 j)
7	4, 6	2an 79	. . . . . . . 8 (b ^ d) = ((a ->1 j) ^ (c ->1 j))
8	7	lor 70	. . . . . . 7 ((a ^ c) v (b ^ d)) = ((a ^ c) v ((a ->1 j) ^ (c ->1 j)))
9		oa8to5.5	. . . . . . . . . . 11 h' = (g ->1 j)'
10	9	con1 66	. . . . . . . . . 10 h = (g ->1 j)
11	4, 10	2an 79	. . . . . . . . 9 (b ^ h) = ((a ->1 j) ^ (g ->1 j))
12	11	lor 70	. . . . . . . 8 ((a ^ g) v (b ^ h)) = ((a ^ g) v ((a ->1 j) ^ (g ->1 j)))
13	6, 10	2an 79	. . . . . . . . 9 (d ^ h) = ((c ->1 j) ^ (g ->1 j))
14	13	lor 70	. . . . . . . 8 ((c ^ g) v (d ^ h)) = ((c ^ g) v ((c ->1 j) ^ (g ->1 j)))
15	12, 14	2an 79	. . . . . . 7 (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h))) = (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j))))
16	8, 15	2or 72	. . . . . 6 (((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) = (((a ^ c) v ((a ->1 j) ^ (c ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((c ^ g) v ((c ->1 j) ^ (g ->1 j)))))
17		oa8to5.4	. . . . . . . . . . 11 f' = (e ->1 j)'
18	17	con1 66	. . . . . . . . . 10 f = (e ->1 j)
19	4, 18	2an 79	. . . . . . . . 9 (b ^ f) = ((a ->1 j) ^ (e ->1 j))
20	19	lor 70	. . . . . . . 8 ((a ^ e) v (b ^ f)) = ((a ^ e) v ((a ->1 j) ^ (e ->1 j)))
21	18, 10	2an 79	. . . . . . . . . 10 (f ^ h) = ((e ->1 j) ^ (g ->1 j))
22	21	lor 70	. . . . . . . . 9 ((e ^ g) v (f ^ h)) = ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))
23	12, 22	2an 79	. . . . . . . 8 (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h))) = (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))
24	20, 23	2or 72	. . . . . . 7 (((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) = (((a ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))))
25	6, 18	2an 79	. . . . . . . . 9 (d ^ f) = ((c ->1 j) ^ (e ->1 j))
26	25	lor 70	. . . . . . . 8 ((c ^ e) v (d ^ f)) = ((c ^ e) v ((c ->1 j) ^ (e ->1 j)))
27	14, 22	2an 79	. . . . . . . 8 (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))) = (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))
28	26, 27	2or 72	. . . . . . 7 (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h)))) = (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))))
29	24, 28	2an 79	. . . . . 6 ((((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 ^ e) v ((a ->1 j) ^ (e ->1 j))) v (((a ^ g) v ((a ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))) ^ (((c ^ e) v ((c ->1 j) ^ (e ->1 j))) v (((c ^ g) v ((c ->1 j) ^ (g ->1 j))) ^ ((e ^ g) v ((e ->1 j) ^ (g ->1 j))))))
30	16, 29	2or 72	. . . . 5 ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f