Theorem oa23 916

Description: Derivation of OA from Godowski/Greechie Eq. II.

Hypothesis

Ref	Expression
oa23.1	(c_|_ ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) =< a_|_

Assertion

Ref	Expression
oa23	((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)

Proof of Theorem oa23

Step	Hyp	Ref	Expression
1		ax-a2 30	. . . . . . 7 (b v c) = (c v b)
2	1	ax-r4 36	. . . . . 6 (b v c)_|_ = (c v b)_|_
3		ancom 68	. . . . . 6 ((a ->2 b) ^ (a ->2 c)) = ((a ->2 c) ^ (a ->2 b))
4	2, 3	2or 67	. . . . 5 ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c))) = ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))
5	4	lan 70	. . . 4 ((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))
6	5	ax-r5 37	. . 3 (((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) v (a ->2 c)) = (((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))) v (a ->2 c))
7		ax-a2 30	. . 3 (((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))) v (a ->2 c)) = ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))
8		ax-a3 31	. . . . . . . . . 10 (((a ->2 c) v (a ->2 c)) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) = ((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))))
9	8	ax-r1 34	. . . . . . . . 9 ((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) = (((a ->2 c) v (a ->2 c)) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))
10		oridm 102	. . . . . . . . . 10 ((a ->2 c) v (a ->2 c)) = (a ->2 c)
11	10	ax-r5 37	. . . . . . . . 9 (((a ->2 c) v (a ->2 c)) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) = ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))
12	9, 11	ax-r2 35	. . . . . . . 8 ((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) = ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))
13		u2lemonb 618	. . . . . . . 8 ((a ->2 c) v c_|_) = 1
14	12, 13	2an 72	. . . . . . 7 (((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) ^ ((a ->2 c) v c_|_)) = (((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) ^ 1)
15	14	ax-r1 34	. . . . . 6 (((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) ^ 1) = (((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) ^ ((a ->2 c) v c_|_))
16		an1 98	. . . . . . 7 (((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) ^ 1) = ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))
17	16	ax-r1 34	. . . . . 6 ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) = (((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) ^ 1)
18		comorr 176	. . . . . . 7 (a ->2 c) C ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))
19		u2lemc1 663	. . . . . . . . 9 c C (a ->2 c)
20	19	comcom 435	. . . . . . . 8 (a ->2 c) C c
21	20	comcom2 175	. . . . . . 7 (a ->2 c) C c_|_
22	18, 21	fh3 453	. . . . . 6 ((a ->2 c) v (((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) ^ c_|_)) = (((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) ^ ((a ->2 c) v c_|_))
23	15, 17, 22	3tr1 60	. . . . 5 ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) = ((a ->2 c) v (((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) ^ c_|_))
24		oa23.1	. . . . . . . . 9 (c_|_ ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) =< a_|_
25		lea 152	. . . . . . . . 9 (c_|_ ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) =< c_|_
26	24, 25	ler2an 165	. . . . . . . 8 (c_|_ ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) =< (a_|_ ^ c_|_)
27		ancom 68	. . . . . . . 8 (((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) ^ c_|_) = (c_|_ ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))))
28		u2lemanb 598	. . . . . . . 8 ((a ->2 c) ^ c_|_) = (a_|_ ^ c_|_)
29	26, 27, 28	le3tr1 132	. . . . . . 7 (((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) ^ c_|_) =< ((a ->2 c) ^ c_|_)
30	29	lelor 158	. . . . . 6 ((a ->2 c) v (((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) ^ c_|_)) =< ((a ->2 c) v ((a ->2 c) ^ c_|_))
31		a5b 112	. . . . . 6 ((a ->2 c) v ((a ->2 c) ^ c_|_)) = (a ->2 c)
32	30, 31	lbtr 131	. . . . 5 ((a ->2 c) v (((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) ^ c_|_)) =< (a ->2 c)
33	23, 32	bltr 130	. . . 4 ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) =< (a ->2 c)
34		leo 150	. . . 4 (a ->2 c) =< ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))
35	33, 34	lebi 137	. . 3 ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b))))) = (a ->2 c)
36	6, 7, 35	3tr 62	. 2 (((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) v (a ->2 c)) = (a ->2 c)
37	36	df-le1 122	1 ((a ->2 b) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7  1wt 9   ->2 wi2 14

This theorem is referenced by:  oa43v 1008  oa63v 1011

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-i2 44  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org