Theorem oa8to5 952

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 951	. 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 63	. . 3 b = (a ->1 j)
5		oa8to5.3	. . . . . . . . . 10 d_|_ = (c ->1 j)_|_
6	5	con1 63	. . . . . . . . 9 d = (c ->1 j)
7	4, 6	2an 72	. . . . . . . 8 (b ^ d) = ((a ->1 j) ^ (c ->1 j))
8	7	lor 66	. . . . . . 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 63	. . . . . . . . . 10 h = (g ->1 j)
11	4, 10	2an 72	. . . . . . . . 9 (b ^ h) = ((a ->1 j) ^ (g ->1 j))
12	11	lor 66	. . . . . . . 8 ((a ^ g) v (b ^ h)) = ((a ^ g) v ((a ->1 j) ^ (g ->1 j)))
13	6, 10	2an 72	. . . . . . . . 9 (d ^ h) = ((c ->1 j) ^ (g ->1 j))
14	13	lor 66	. . . . . . . 8 ((c ^ g) v (d ^ h)) = ((c ^ g) v ((c ->1 j) ^ (g ->1 j)))
15	12, 14	2an 72	. . . . . . 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 67	. . . . . 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 63	. . . . . . . . . 10 f = (e ->1 j)
19	4, 18	2an 72	. . . . . . . . 9 (b ^ f) = ((a ->1 j) ^ (e ->1 j))
20	19	lor 66	. . . . . . . 8 ((a ^ e) v (b ^ f)) = ((a ^ e) v ((a ->1 j) ^ (e ->1 j)))
21	18, 10	2an 72	. . . . . . . . . 10 (f ^ h) = ((e ->1 j) ^ (g ->1 j))
22	21	lor 66	. . . . . . . . 9 ((e ^ g) v (f ^ h)) = ((e ^ g) v ((e ->1 j) ^ (g ->1 j)))
23	12, 22	2an 72	. . . . . . . 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 67	. . . . . . 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 72	. . . . . . . . 9 (d ^ f) = ((c ->1 j) ^ (e ->1 j))
26	25	lor 66	. . . . . . . 8 ((c ^ e) v (d ^ f)) = ((c ^ e) v ((c ->1 j) ^ (e ->1 j)))
27	14, 22	2an 72	. . . . . . . 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 67	. . . . . . 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 72	. . . . . 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 67	. . . . 5 ((((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))