Theorem oa4uto4 957

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

Hypothesis

Ref	Expression
oa4uto4.1	((a ->1 d) ^ ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->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)))))))) =< d

Assertion

Ref	Expression
oa4uto4	((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< d

Proof of Theorem oa4uto4

Step	Hyp	Ref	Expression
1		u1lem9a 759	. . . . 5 (a_|_ ->1 d)_|_ =< a_|_
2	1	lecon1 147	. . . 4 a =< (a_|_ ->1 d)
3		u1lem9a 759	. . . . . 6 (b_|_ ->1 d)_|_ =< b_|_
4	3	lecon1 147	. . . . 5 b =< (b_|_ ->1 d)
5		ax-a2 30	. . . . . . 7 ((a ^ b) v ((a ->1 d) ^ (b ->1 d))) = (((a ->1 d) ^ (b ->1 d)) v (a ^ b))
6	2, 4	le2an 161	. . . . . . . 8 (a ^ b) =< ((a_|_ ->1 d) ^ (b_|_ ->1 d))
7	6	lelor 158	. . . . . . 7 (((a ->1 d) ^ (b ->1 d)) v (a ^ b)) =< (((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->1 d)))
8	5, 7	bltr 130	. . . . . 6 ((a ^ b) v ((a ->1 d) ^ (b ->1 d))) =< (((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->1 d)))
9		ax-a2 30	. . . . . . . 8 ((a ^ c) v ((a ->1 d) ^ (c ->1 d))) = (((a ->1 d) ^ (c ->1 d)) v (a ^ c))
10		u1lem9a 759	. . . . . . . . . . 11 (c_|_ ->1 d)_|_ =< c_|_
11	10	lecon1 147	. . . . . . . . . 10 c =< (c_|_ ->1 d)
12	2, 11	le2an 161	. . . . . . . . 9 (a ^ c) =< ((a_|_ ->1 d) ^ (c_|_ ->1 d))
13	12	lelor 158	. . . . . . . 8 (((a ->1 d) ^ (c ->1 d)) v (a ^ c)) =< (((a ->1 d) ^ (c ->1 d)) v ((a_|_ ->1 d) ^ (c_|_ ->1 d)))
14	9, 13	bltr 130	. . . . . . 7 ((a ^ c) v ((a ->1 d) ^ (c ->1 d))) =< (((a ->1 d) ^ (c ->1 d)) v ((a_|_ ->1 d) ^ (c_|_ ->1 d)))
15		ax-a2 30	. . . . . . . 8 ((b ^ c) v ((b ->1 d) ^ (c ->1 d))) = (((b ->1 d) ^ (c ->1 d)) v (b ^ c))
16	4, 11	le2an 161	. . . . . . . . 9 (b ^ c) =< ((b_|_ ->1 d) ^ (c_|_ ->1 d))
17	16	lelor 158	. . . . . . . 8 (((b ->1 d) ^ (c ->1 d)) v (b ^ c)) =< (((b ->1 d) ^ (c ->1 d)) v ((b_|_ ->1 d) ^ (c_|_ ->1 d)))
18	15, 17	bltr 130	. . . . . . 7 ((b ^ c) v ((b ->1 d) ^ (c ->1 d))) =< (((b ->1 d) ^ (c ->1 d)) v ((b_|_ ->1 d) ^ (c_|_ ->1 d)))
19	14, 18	le2an 161	. . . . . 6 (((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))))
20	8, 19	le2or 160	. . . . 5 (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))) =< ((((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->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)))))
21	4, 20	le2an 161	. . . 4 (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))) =< ((b_|_ ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->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))))))
22	2, 21	le2or 160	. . 3 (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))))) =< ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->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)))))))
23	22	lelan 159	. 2 ((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< ((a ->1 d) ^ ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->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		oa4uto4.1	. 2 ((a ->1 d) ^ ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->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)))))))) =< d
25	23, 24	letr 129	1 ((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< d

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->1 wi1 13

This theorem is referenced by:  d6oa 977  axoa4 1013

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-t 40  df-f 41  df-i1 43  df-le1 122  df-le2 123

metamath.org