Theorem 5oa 9601

Description: Orthoarguesian law 5OA. This 8-variable inference is called 5OA because it can be converted to a 5-variable equation (see Quantum Logic Explorer).

Hypotheses

Ref	Expression
5oa.1	|- A e. CH
5oa.2	|- B e. CH
5oa.3	|- C e. CH
5oa.4	|- D e. CH
5oa.5	|- F e. CH
5oa.6	|- G e. CH
5oa.7	|- R e. CH
5oa.8	|- S e. CH
5oa.9	|- A (_ (_|_` B)
5oa.10	|- C (_ (_|_` D)
5oa.11	|- F (_ (_|_` G)
5oa.12	|- R (_ (_|_` S)

Assertion

Ref	Expression
5oa	|- (((A vH B) i^i (C vH D)) i^i ((F vH G) i^i (R vH S))) (_ (B vH (A i^i (C vH ((((A vH C) i^i (B vH D)) i^i (((A vH R) i^i (B vH S)) vH ((C vH R) i^i (D vH S)))) i^i ((((A vH F) i^i (B vH G)) i^i (((A vH R) i^i (B vH S)) vH ((F vH R) i^i (G vH S)))) vH (((C vH F) i^i (D vH G)) i^i (((C vH R) i^i (D vH S)) vH ((F vH R) i^i (G vH S)))))))))

Proof of Theorem 5oa

Step	Hyp	Ref	Expression
1		5oa.9	. . . . . 6 |- A (_ (_|_` B)
2		5oa.1	. . . . . . 7 |- A e. CH
3		5oa.2	. . . . . . 7 |- B e. CH
4	2, 3	osum 9581	. . . . . 6 |- (A (_ (_|_` B) -> (A +H B) = (A vH B))
5	1, 4	ax-mp 7	. . . . 5 |- (A +H B) = (A vH B)
6		5oa.10	. . . . . 6 |- C (_ (_|_` D)
7		5oa.3	. . . . . . 7 |- C e. CH
8		5oa.4	. . . . . . 7 |- D e. CH
9	7, 8	osum 9581	. . . . . 6 |- (C (_ (_|_` D) -> (C +H D) = (C vH D))
10	6, 9	ax-mp 7	. . . . 5 |- (C +H D) = (C vH D)
11	5, 10	ineq12i 2218	. . . 4 |- ((A +H B) i^i (C +H D)) = ((A vH B) i^i (C vH D))
12		5oa.11	. . . . . 6 |- F (_ (_|_` G)
13		5oa.5	. . . . . . 7 |- F e. CH
14		5oa.6	. . . . . . 7 |- G e. CH
15	13, 14	osum 9581	. . . . . 6 |- (F (_ (_|_` G) -> (F +H G) = (F vH G))
16	12, 15	ax-mp 7	. . . . 5 |- (F +H G) = (F vH G)
17		5oa.12	. . . . . 6 |- R (_ (_|_` S)
18		5oa.7	. . . . . . 7 |- R e. CH
19		5oa.8	. . . . . . 7 |- S e. CH
20	18, 19	osum 9581	. . . . . 6 |- (R (_ (_|_` S) -> (R +H S) = (R vH S))
21	17, 20	ax-mp 7	. . . . 5 |- (R +H S) = (R vH S)
22	16, 21	ineq12i 2218	. . . 4 |- ((F +H G) i^i (R +H S)) = ((F vH G) i^i (R vH S))
23	11, 22	ineq12i 2218	. . 3 |- (((A +H B) i^i (C +H D)) i^i ((F +H G) i^i (R +H S))) = (((A vH B) i^i (C vH D)) i^i ((F vH G) i^i (R vH S)))
24	2	chshi 9092	. . . 4 |- A e. SH
25	3	chshi 9092	. . . 4 |- B e. SH
26	7	chshi 9092	. . . 4 |- C e. SH
27	8	chshi 9092	. . . 4 |- D e. SH
28	13	chshi 9092	. . . 4 |- F e. SH
29	14	chshi 9092	. . . 4 |- G e. SH
30	18	chshi 9092	. . . 4 |- R e. SH
31	19	chshi 9092	. . . 4 |- S e. SH
32	24, 25, 26, 27, 28, 29, 30, 31	5oalem7 9600	. . 3 |- (((A +H B) i^i (C +H D)) i^i ((F +H G) i^i (R +H S))) (_ (B +H (A i^i (C +H ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S)))))))))
33	23, 32	eqsstr3 2095	. 2 |- (((A vH B) i^i (C vH D)) i^i ((F vH G) i^i (R vH S))) (_ (B +H (A i^i (C +H ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S)))))))))
34	24, 26	shscl 9276	. . . . . . . . 9 |- (A +H C) e. SH
35	25, 27	shscl 9276	. . . . . . . . 9 |- (B +H D) e. SH
36	34, 35	shincl 9326	. . . . . . . 8 |- ((A +H C) i^i (B +H D)) e. SH
37	24, 30	shscl 9276	. . . . . . . . . 10 |- (A +H R) e. SH
38	25, 31	shscl 9276	. . . . . . . . . 10 |- (B +H S) e. SH
39	37, 38	shincl 9326	. . . . . . . . 9 |- ((A +H R) i^i (B +H S)) e. SH
40	26, 30	shscl 9276	. . . . . . . . . 10 |- (C +H R) e. SH
41	27, 31	shscl 9276	. . . . . . . . . 10 |- (D +H S) e. SH
42	40, 41	shincl 9326	. . . . . . . . 9 |- ((C +H R) i^i (D +H S)) e. SH
43	39, 42	shscl 9276	. . . . . . . 8 |- (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S))) e. SH
44	36, 43	shincl 9326	. . . . . . 7 |- (((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) e. SH
45	24, 28	shscl 9276	. . . . . . . . . 10 |- (A +H F) e. SH
46	25, 29	shscl 9276	. . . . . . . . . 10 |- (B +H G) e. SH
47	45, 46	shincl 9326	. . . . . . . . 9 |- ((A +H F) i^i (B +H G)) e. SH
48	28, 30	shscl 9276	. . . . . . . . . . 11 |- (F +H R) e. SH
49	29, 31	shscl 9276	. . . . . . . . . . 11 |- (G +H S) e. SH
50	48, 49	shincl 9326	. . . . . . . . . 10 |- ((F +H R) i^i (G +H S)) e. SH
51	39, 50	shscl 9276	. . . . . . . . 9 |- (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S))) e. SH
52	47, 51	shincl 9326	. . . . . . . 8 |- (((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) e. SH
53	26, 28	shscl 9276	. . . . . . . . . 10 |- (C +H F) e. SH
54	27, 29	shscl 9276	. . . . . . . . . 10 |- (D +H G) e. SH
55	53, 54	shincl 9326	. . . . . . . . 9 |- ((C +H F) i^i (D +H G)) e. SH
56	42, 50	shscl 9276	. . . . . . . . 9 |- (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S))) e. SH
57	55, 56	shincl 9326	. . . . . . . 8 |- (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S)))) e. SH
58	52, 57	shscl 9276	. . . . . . 7 |- ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S))))) e. SH
59	44, 58	shincl 9326	. . . . . 6 |- ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S)))))) e. SH
60	26, 59	shscl 9276	. . . . 5 |- (C +H ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S))))))) e. SH
61	24, 60	shincl 9326	. . . 4 |- (A i^i (C +H ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S)))))))) e. SH
62	25, 61	shslej 9333	. . 3 |- (B +H (A i^i (C +H ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H