Theorem oa4uto4g 955

Description: Derivation of "Godowski/Greechie" 4-variable proper OA law variant from "universal" variant oa4to4u2 954.

Hypotheses

Ref	Expression
oa4uto4g.1	((b_|_ ->1 d) ^ ((b_|__|_ ->1 d) v ((a_|__|_ ->1 d) ^ ((((b_|_ ->1 d) ^ (a_|_ ->1 d)) v ((b_|__|_ ->1 d) ^ (a_|__|_ ->1 d))) v ((((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b_|__|_ ->1 d) ^ (c_|__|_ ->1 d))) ^ (((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a_|__|_ ->1 d) ^ (c_|__|_ ->1 d)))))))) =< d
oa4uto4g.4	h = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))

Assertion

Ref	Expression
oa4uto4g	((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h)) =< (b ->1 d)

Proof of Theorem oa4uto4g

Step	Hyp	Ref	Expression
1		ancom 68	. . . . . . . 8 (a ^ b) = (b ^ a)
2		ancom 68	. . . . . . . 8 ((a ->1 d) ^ (b ->1 d)) = ((b ->1 d) ^ (a ->1 d))
3	1, 2	2or 67	. . . . . . 7 ((a ^ b) v ((a ->1 d) ^ (b ->1 d))) = ((b ^ a) v ((b ->1 d) ^ (a ->1 d)))
4	3	ax-r5 37	. . . . . 6 (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h) = (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h)
5	4	lan 70	. . . . 5 ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h)) = ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h))
6	5	lor 66	. . . 4 ((b ->1 d) v ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h))) = ((b ->1 d) v ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h)))
7	6	lan 70	. . 3 (b ^ ((b ->1 d) v ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h)))) = (b ^ ((b ->1 d) v ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h))))
8		u1lem9a 759	. . . . . 6 (b_|_ ->1 d)_|_ =< b_|_
9	8	lecon1 147	. . . . 5 b =< (b_|_ ->1 d)
10		u1lem9a 759	. . . . . . . . . . 11 (a_|_ ->1 d)_|_ =< a_|_
11	10	lecon1 147	. . . . . . . . . 10 a =< (a_|_ ->1 d)
12	9, 11	le2an 161	. . . . . . . . 9 (b ^ a) =< ((b_|_ ->1 d) ^ (a_|_ ->1 d))
13	12	leror 144	. . . . . . . 8 ((b ^ a) v ((b ->1 d) ^ (a ->1 d))) =< (((b_|_ ->1 d) ^ (a_|_ ->1 d)) v ((b ->1 d) ^ (a ->1 d)))
14		oa4uto4g.4	. . . . . . . . 9 h = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
15		u1lem9a 759	. . . . . . . . . . . . 13 (c_|_ ->1 d)_|_ =< c_|_
16	15	lecon1 147	. . . . . . . . . . . 12 c =< (c_|_ ->1 d)
17	11, 16	le2an 161	. . . . . . . . . . 11 (a ^ c) =< ((a_|_ ->1 d) ^ (c_|_ ->1 d))
18	17	leror 144	. . . . . . . . . 10 ((a ^ c) v ((a ->1 d) ^ (c ->1 d))) =< (((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a ->1 d) ^ (c ->1 d)))
19	9, 16	le2an 161	. . . . . . . . . . 11 (b ^ c) =< ((b_|_ ->1 d) ^ (c_|_ ->1 d))
20	19	leror 144	. . . . . . . . . 10 ((b ^ c) v ((b ->1 d) ^ (c ->1 d))) =< (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b ->1 d) ^ (c ->1 d)))
21	18, 20	le2an 161	. . . . . . . . 9 (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))) =< ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a ->1 d) ^ (c ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b ->1 d) ^ (c ->1 d))))
22	14, 21	bltr 130	. . . . . . . 8 h =< ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a ->1 d) ^ (c ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b ->1 d) ^ (c ->1 d))))
23	13, 22	le2or 160	. . . . . . 7 (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h) =< ((((b_|_ ->1 d) ^ (a_|_ ->1 d)) v ((b ->1 d) ^ (a ->1 d))) v ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a ->1 d) ^ (c ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b ->1 d) ^ (c ->1 d)))))
24	23	lelan 159	. . . . . 6 ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h)) =< ((a ->1 d) ^ ((((b_|_ ->1 d) ^ (a_|_ ->1 d)) v ((b ->1 d) ^ (a ->1 d))) v ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a ->1 d) ^ (c ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b ->1 d) ^ (c ->1 d))))))
25	24	lelor 158	. . . . 5 ((b ->1 d) v ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h))) =< ((b ->1 d) v ((a ->1 d) ^ ((((b_|_ ->1 d) ^ (a_|_ ->1 d)) v ((b ->1 d) ^ (a ->1 d))) v ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a ->1 d) ^ (c ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b ->1 d) ^ (c ->1 d)))))))
26	9, 25	le2an 161	. . . 4 (b ^ ((b ->1 d) v ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h)))) =< ((b_|_ ->1 d) ^ ((b ->1 d) v ((a ->1 d) ^ ((((b_|_ ->1 d) ^ (a_|_ ->1 d)) v ((b ->1 d) ^ (a ->1 d))) v ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a ->1 d) ^ (c ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b ->1 d) ^ (c ->1 d))))))))
27		ax-a1 29	. . . . . . . 8 b = b_|__|_
28	27	ud1lem0b 248	. . . . . . 7 (b ->1 d) = (b_|__|_ ->1 d)
29		ax-a1 29	. . . . . . . . 9 a = a_|__|_
30	29	ud1lem0b 248	. . . . . . . 8 (a ->1 d) = (a_|__|_ ->1 d)
31	28, 30	2an 72	. . . . . . . . . 10 ((b ->1 d) ^ (a ->1 d)) = ((b_|__|_ ->1 d) ^ (a_|__|_ ->1 d))
32	31	lor 66	. . . . . . . . 9 (((b_|_ ->1 d) ^ (a_|_ ->1 d)) v ((b ->1 d) ^ (a ->1 d))) = (((b_|_ ->1 d) ^ (a_|_ ->1 d)) v ((b_|__|_ ->1 d) ^ (a_|__|_ ->1 d)))
33		ancom 68	. . . . . . . . . 10 ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a ->1 d) ^ (c ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b ->1 d) ^ (c ->1 d)))) = ((((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b ->1 d) ^ (c ->1 d))) ^ (((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a ->1 d) ^ (c ->1 d))))
34		ax-a1 29	. . . . . . . . . . . . . 14 c = c_|__|_
35	34	ud1lem0b 248	. . . . . . . . . . . . 13 (c ->1 d) = (c_|__|_ ->1 d)
36	28, 35	2an 72	. . . . . . . . . . . 12 ((b ->1 d) ^ (c ->1 d)) = ((b_|__|_ ->1 d) ^ (c_|__|_ ->1 d))
37	36	lor 66	. . . . . . . . . . 11 (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b ->1 d) ^ (c ->1 d))) = (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v ((b_|__|_ ->1 d) ^ (c_|__|_ ->1 d)))
38	30, 35	2an 72	. . . . . . . . . . . 12 ((a ->1 d) ^ (c ->1 d)) = ((a_|__|_ ->1 d) ^ (c_|__|_ ->1 d))
39	38	lor 66	. . . . . . . . . . 11 (((a_|_ ->1 d) ^ (c_|_ ->1 d)) v ((a ->1 d) ^ (c ->1 d))) = (((a_|_ ->1 d) ^ (c_|_