Theorem oa3-2to4 968

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

Hypothesis

Ref	Expression
oa3-2to4.1	((a ->1 c) ^ (a v (b ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))) =< c

Assertion

Ref	Expression
oa3-2to4	(a_|_ ^ (a v (b ^ ((a == b) v ((a ->1 c) ^ (b ->1 c)))))) =< c

Proof of Theorem oa3-2to4

Step	Hyp	Ref	Expression
1		oa3-4lem 963	. . 3 (a_|_ ^ (a v (b ^ (((a ^ b) v (a_|_ ^ b_|_)) v (((a ^ c) v (a_|_ ^ 1)) ^ ((b ^ c) v (b_|_ ^ 1))))))) = (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 ^ c) v (a_|_ ^ 1)) ^ ((b ^ c) v (b_|_ ^ 1)))))))
3		leid 140	. . 3 a_|_ =< a_|_
4		leid 140	. . 3 b_|_ =< b_|_
5		le1 138	. . 3 c_|_ =< 1
6		an1 98	. . . . . . 7 (c ^ 1) = c
7		dff 93	. . . . . . . . . 10 0 = (a ^ a_|_)
8		dff 93	. . . . . . . . . 10 0 = (b ^ b_|_)
9	7, 8	2or 67	. . . . . . . . 9 (0 v 0) = ((a ^ a_|_) v (b ^ b_|_))
10	9	ax-r1 34	. . . . . . . 8 ((a ^ a_|_) v (b ^ b_|_)) = (0 v 0)
11		or0 94	. . . . . . . 8 (0 v 0) = 0
12	10, 11	ax-r2 35	. . . . . . 7 ((a ^ a_|_) v (b ^ b_|_)) = 0
13	6, 12	2or 67	. . . . . 6 ((c ^ 1) v ((a ^ a_|_) v (b ^ b_|_))) = (c v 0)
14		or0 94	. . . . . 6 (c v 0) = c
15	13, 14	ax-r2 35	. . . . 5 ((c ^ 1) v ((a ^ a_|_) v (b ^ b_|_))) = c
16	15	ax-r1 34	. . . 4 c = ((c ^ 1) v ((a ^ a_|_) v (b ^ b_|_)))
17		ax-a2 30	. . . 4 ((c ^ 1) v ((a ^ a_|_) v (b ^ b_|_))) = (((a ^ a_|_) v (b ^ b_|_)) v (c ^ 1))
18	16, 17	ax-r2 35	. . 3 c = (((a ^ a_|_) v (b ^ b_|_)) v (c ^ 1))
19		oa3-2lemb 959	. . . 4 ((a ->1 c) ^ (a v (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ c) v ((a ->1 c) ^ (c ->1 c))) ^ ((b ^ c) v ((b ->1 c) ^ (c ->1 c)))))))) = ((a ->1 c) ^ (a v (b ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))
20		oa3-2to4.1	. . . 4 ((a ->1 c) ^ (a v (b ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))) =< c
21	19, 20	bltr 130	. . 3 ((a ->1 c) ^ (a v (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ c) v ((a ->1 c) ^ (c ->1 c))) ^ ((b ^ c) v ((b ->1 c) ^ (c ->1 c)))))))) =< c
22	3, 4, 5, 18, 21	oa4to6dual 944	. 2 (a_|_ ^ (a v (b ^ (((a ^ b) v (a_|_ ^ b_|_)) v (((a ^ c) v (a_|_ ^ 1)) ^ ((b ^ c) v (b_|_ ^ 1))))))) =< c
23	2, 22	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