Theorem mlaconj4 844

Description: For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30) in OA-GO paper.

Hypotheses

Ref	Expression
mlaconj4.1	((d == e) ^ ((e' ^ c') v (d ^ c))) =< (d == c)
mlaconj4.2	d = (a v b)
mlaconj4.3	e = (a ^ b)

Assertion

Ref	Expression
mlaconj4	((a == b) ^ ((a == c) v (b == c))) =< (a == c)

Proof of Theorem mlaconj4

Step	Hyp	Ref	Expression
1		biao 799	. . . . 5 (a == b) = ((a ^ b) == (a v b))
2		bicom 96	. . . . 5 ((a ^ b) == (a v b)) = ((a v b) == (a ^ b))
3	1, 2	ax-r2 36	. . . 4 (a == b) = ((a v b) == (a ^ b))
4	3	bile 142	. . 3 (a == b) =< ((a v b) == (a ^ b))
5		orbile 843	. . . 4 ((a == c) v (b == c)) =< (((a ^ b) ->2 c) ^ (c ->1 (a v b)))
6		imp3 841	. . . 4 (((a ^ b) ->2 c) ^ (c ->1 (a v b))) = (((a ^ b)' ^ c') v (c ^ (a v b)))
7	5, 6	lbtr 139	. . 3 ((a == c) v (b == c)) =< (((a ^ b)' ^ c') v (c ^ (a v b)))
8	4, 7	le2an 169	. 2 ((a == b) ^ ((a == c) v (b == c))) =< (((a v b) == (a ^ b)) ^ (((a ^ b)' ^ c') v (c ^ (a v b))))
9		mlaconj4.2	. . . . . 6 d = (a v b)
10		mlaconj4.3	. . . . . 6 e = (a ^ b)
11	9, 10	2bi 99	. . . . 5 (d == e) = ((a v b) == (a ^ b))
12	10	ax-r4 37	. . . . . . 7 e' = (a ^ b)'
13	12	ran 78	. . . . . 6 (e' ^ c') = ((a ^ b)' ^ c')
14		ancom 74	. . . . . . 7 (d ^ c) = (c ^ d)
15	9	lan 77	. . . . . . 7 (c ^ d) = (c ^ (a v b))
16	14, 15	ax-r2 36	. . . . . 6 (d ^ c) = (c ^ (a v b))
17	13, 16	2or 72	. . . . 5 ((e' ^ c') v (d ^ c)) = (((a ^ b)' ^ c') v (c ^ (a v b)))
18	11, 17	2an 79	. . . 4 ((d == e) ^ ((e' ^ c') v (d ^ c))) = (((a v b) == (a ^ b)) ^ (((a ^ b)' ^ c') v (c ^ (a v b))))
19	18	ax-r1 35	. . 3 (((a v b) == (a ^ b)) ^ (((a ^ b)' ^ c') v (c ^ (a v b)))) = ((d == e) ^ ((e' ^ c') v (d ^ c)))
20		lea 160	. . . . . 6 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< (d == e)
21		bicom 96	. . . . . . 7 ((a v b) == (a ^ b)) = ((a ^ b) == (a v b))
22	21, 11, 1	3tr1 63	. . . . . 6 (d == e) = (a == b)
23	20, 22	lbtr 139	. . . . 5 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< (a == b)
24		mlaconj4.1	. . . . . 6 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< (d == c)
25	9	rbi 98	. . . . . 6 (d == c) = ((a v b) == c)
26	24, 25	lbtr 139	. . . . 5 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< ((a v b) == c)
27	23, 26	ler2an 173	. . . 4 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< ((a == b) ^ ((a v b) == c))
28		anass 76	. . . . . . . . . . 11 ((a' ^ b') ^ c') = (a' ^ (b' ^ c'))
29		coman1 185	. . . . . . . . . . . 12 (a' ^ (b' ^ c')) C a'
30	29	comcom7 460	. . . . . . . . . . 11 (a' ^ (b' ^ c')) C a
31	28, 30	bctr 181	. . . . . . . . . 10 ((a' ^ b') ^ c') C a
32		an32 83	. . . . . . . . . . 11 ((a' ^ b') ^ c') = ((a' ^ c') ^ b')
33		coman2 186	. . . . . . . . . . . 12 ((a' ^ c') ^ b') C b'
34	33	comcom7 460	. . . . . . . . . . 11 ((a' ^ c') ^ b') C b
35	32, 34	bctr 181	. . . . . . . . . 10 ((a' ^ b') ^ c') C b
36	31, 35	com2an 484	. . . . . . . . 9 ((a' ^ b') ^ c') C (a ^ b)
37		coman1 185	. . . . . . . . 9 ((a' ^ b') ^ c') C (a' ^ b')
38	36, 37	com2or 483	. . . . . . . 8 ((a' ^ b') ^ c') C ((a ^ b) v (a' ^ b'))
39	31, 35	com2or 483	. . . . . . . . 9 ((a' ^ b') ^ c') C (a v b)
40		coman2 186	. . . . . . . . . 10 ((a' ^ b') ^ c') C c'
41	40	comcom7 460	. . . . . . . . 9 ((a' ^ b') ^ c') C c
42	39, 41	com2an 484	. . . . . . . 8 ((a' ^ b') ^ c') C ((a v b) ^ c)
43	38, 42	fh2c 477	. . . . . . 7 (((a ^ b) v (a' ^ b')) ^ (((a v b) ^ c) v ((a' ^ b') ^ c'))) = ((((a ^ b) v (a' ^ b')) ^ ((a v b) ^ c)) v (((a ^ b) v (a' ^ b')) ^ ((a' ^ b') ^ c')))
44		anor3 90	. . . . . . . . . . 11 (a' ^ b') = (a v b)'
45		comanr1 464	. . . . . . . . . . . 12 (a v b) C ((a v b) ^ c)
46	45	comcom3 454	. . . . . . . . . . 11 (a v b)' C ((a v b) ^ c)
47	44, 46	bctr 181	. . . . . . . . . 10 (a' ^ b') C ((a v b) ^ c)
48		coman1 185	. . . . . . . . . . . 12 (a' ^ b') C a'
49	48	comcom7 460	. . . . . . . . . . 11 (a' ^ b') C a
50		coman2 186	. . . . . . . . . . . 12 (a' ^ b') C b'
51	50	comcom7 460	. . . . . . . . . . 11 (a' ^ b') C b
52	49, 51	com2an 484	. . . . . . . . . 10 (a' ^ b') C (a ^ b)
53	47, 52	fh2rc 480	. . . . . . . . 9 (((a ^ b) v (a' ^ b')) ^ ((a v b) ^ c)) = (((a ^ b) ^ ((a v b) ^ c)) v ((a' ^ b') ^ ((a v b) ^ c)))
54		anass 76	. . . . . . . . . . . 12 (((a ^ b) ^ (a v b)) ^ c) = ((a ^ b) ^ ((a v b) ^ c))
55	54	ax-r1 35	. . . . . . . . . . 11 ((a ^ b) ^ ((a v b) ^ c)) = (((a ^ b) ^ (a v b)) ^ c)
56		leao1 162	. . . . . . . . . . . . 13 (a ^ b) =< (a v b)
57	56	df2le2 136	. . . . . . . . . . . 12 ((a ^ b) ^ (a v b)) = (a ^ b)
58	57	ran 78	. . . . . . . . . . 11 (((a ^ b) ^ (a v b)) ^ c) = ((a ^ b) ^ c)
59	55, 58	ax-r2 36	. . . . . . . . . 10 ((a ^ b) ^ ((a v b) ^ c)) = ((a ^ b) ^ c)
60		dff 101	. . . . . . . . . . . . . 14 0 = ((a' ^ b') ^ (a' ^ b')')
61		oran 87	. . . . . . . . . . . . . . . 16 (a v b) = (a' ^ b')'
62	61	lan 77	. . . . . . . . . . . . . . 15 ((a' ^ b') ^ (a v b)) = ((a' ^ b') ^ (a' ^ b')')
63	62	ax-r1 35	. . . . . . . . . . . . . 14 ((a' ^ b') ^ (a' ^ b')') = ((a' ^ b') ^ (a v b))
64	60, 63	ax-r2 36	. . . . . . . . . . . . 13 0 = ((a' ^ b') ^ (a v b))
65	64	ran 78	. . . . . . . . . . . 12 (0 ^ c) = (((a' ^ b') ^ (a v b)) ^ c)
66	65	ax-r1 35	. . . . . . . . . . 11 (((a' ^ b') ^ (a v b)) ^ c) = (0 ^ c)
67		anass 76	. . . . . . . . . . 11 (((a' ^ b') ^ (a v b)) ^ c) = ((a' ^ b') ^ ((a v b) ^ c))
68		an0r 109	. . . . . . . . . . 11 (0 ^ c) = 0
69	66, 67, 68	3tr2 64	. . . . . . . . . 10 ((a' ^ b') ^ ((a v b) ^ c)) = 0
70	59, 69	2or 72	. . . . . . . . 9 (((a ^ b) ^ ((a v b) ^ c)) v ((a' ^ b') ^ ((a v b) ^ c))) = (((a ^ b) ^ c) v 0)
71		or0 102	. . . . . . . . 9 (((a ^ b) ^ c) v 0) = ((a ^ b) ^ c)
72	53, 70, 71	3tr 65	. . . . . . . 8 (((a ^ b) v (a' ^ b')) ^ ((a v b) ^ c)) = ((a ^ b) ^ c)
73		comanr1 464	. . . . . . . . . 10 (a' ^ b') C ((a' ^ b') ^ c')
74	73, 52	fh2rc 480	. . . . . . . . 9 (((a ^ b) v (a' ^ b')) ^ ((a' ^ b') ^ c')) = (((a ^ b) ^ ((a' ^ b') ^ c')) v ((a' ^ b') ^ ((a' ^ b') ^ c')))
75		an4 86	. . . . . . . . . . 11 ((a ^ b) ^ ((a' ^ b') ^ c')) = ((a ^ (a' ^ b')) ^ (b ^ c'))
76