Theorem oa3-6to3 967

Description: Derivation of 3-OA variant (3) from (6).

Hypothesis

Ref	Expression
oa3-6to3.1	((a ->1 c) ^ (a v (b ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))) =< c

Assertion

Ref	Expression
oa3-6to3	(a_|_ ^ (a v (b ^ ((a == b) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))) =< c

Proof of Theorem oa3-6to3

Step	Hyp	Ref	Expression
1		oa3-3lem 961	. . 3 (a_|_ ^ (a v (b ^ (((a ^ b) v (a_|_ ^ b_|_)) v (((a ^ 1) v (a_|_ ^ c)) ^ ((b ^ 1) v (b_|_ ^ c))))))) = (a_|_ ^ (a v (b ^ ((a == b) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))))
2	1	ax-r1 34	. 2 (a_|_ ^ (a v (b ^ ((a == b) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))) = (a_|_ ^ (a v (b ^ (((a ^ b) v (a_|_ ^ b_|_)) v (((a ^ 1) v (a_|_ ^ c)) ^ ((b ^ 1) v (b_|_ ^ c)))))))
3		leid 140	. . 3 a_|_ =< a_|_
4		leid 140	. . 3 b_|_ =< b_|_
5		df-f 41	. . . . 5 0 = 1_|_
6	5	ax-r1 34	. . . 4 1_|_ = 0
7		le0 139	. . . 4 0 =< c
8	6, 7	bltr 130	. . 3 1_|_ =< c
9		ancom 68	. . . . . . . 8 (1 ^ c) = (c ^ 1)
10		an1 98	. . . . . . . 8 (c ^ 1) = c
11	9, 10	ax-r2 35	. . . . . . 7 (1 ^ c) = c
12		dff 93	. . . . . . . . . 10 0 = (a ^ a_|_)
13		dff 93	. . . . . . . . . 10 0 = (b ^ b_|_)
14	12, 13	2or 67	. . . . . . . . 9 (0 v 0) = ((a ^ a_|_) v (b ^ b_|_))
15	14	ax-r1 34	. . . . . . . 8 ((a ^ a_|_) v (b ^ b_|_)) = (0 v 0)
16		or0 94	. . . . . . . 8 (0 v 0) = 0
17	15, 16	ax-r2 35	. . . . . . 7 ((a ^ a_|_) v (b ^ b_|_)) = 0
18	11, 17	2or 67	. . . . . 6 ((1 ^ c) v ((a ^ a_|_) v (b ^ b_|_))) = (c v 0)
19		or0 94	. . . . . 6 (c v 0) = c
20	18, 19	ax-r2 35	. . . . 5 ((1 ^ c) v ((a ^ a_|_) v (b ^ b_|_))) = c
21	20	ax-r1 34	. . . 4 c = ((1 ^ c) v ((a ^ a_|_) v (b ^ b_|_)))
22		ax-a2 30	. . . 4 ((1 ^ c) v ((a ^ a_|_) v (b ^ b_|_))) = (((a ^ a_|_) v (b ^ b_|_)) v (1 ^ c))
23	21, 22	ax-r2 35	. . 3 c = (((a ^ a_|_) v (b ^ b_|_)) v (1 ^ c))
24		oa3-6lem 960	. . . 4 ((a ->1 c) ^ (a v (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ 1) v ((a ->1 c) ^ (1 ->1 c))) ^ ((b ^ 1) v ((b ->1 c) ^ (1 ->1 c)))))))) = ((a ->1 c) ^ (a v (b ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c))))))
25		oa3-6to3.1	. . . 4 ((a ->1 c) ^ (a v (b ^ (((a_|_ ->1 c) ^ (b_|_ ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))) =< c
26	24, 25	bltr 130	. . 3 ((a ->1 c) ^ (a v (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ 1) v ((a ->1 c) ^ (1 ->1 c))) ^ ((b ^ 1) v ((b ->1 c) ^ (1 ->1 c)))))))) =< c
27	3, 4, 8, 23, 26	oa4to6dual 944	. 2 (a_|_ ^ (a v (b ^ (((a ^ b) v (a_|_ ^ b_|_)) v (((a ^ 1) v (a_|_ ^ c)) ^ ((b ^ 1) v (b_|_ ^ c))))))) =< c
28	2, 27	bltr 130	1 (a_|_ ^ (a v (b ^ ((a == b) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))) =< c

Syntax hints:   =< wle 2  _|_wn 4   == tb 5   v wo 6   ^ wa 7  1wt 9  0wf 10   ->1 wi1 13

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org