Theorem mlaconjo 868

Description: OML proof of Mladen's conjecture.

Assertion

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

Proof of Theorem mlaconjo

Step	Hyp	Ref	Expression
1		dfb 86	. . . 4 (a == b) = ((a ^ b) v (a_|_ ^ b_|_))
2	1	bile 134	. . 3 (a == b) =< ((a ^ b) v (a_|_ ^ b_|_))
3		mlaconjolem 867	. . 3 ((a == c) v (b == c)) =< ((c ^ (a v b)) v (c_|_ ^ (a_|_ v b_|_)))
4	2, 3	le2an 161	. 2 ((a == b) ^ ((a == c) v (b == c))) =< (((a ^ b) v (a_|_ ^ b_|_)) ^ ((c ^ (a v b)) v (c_|_ ^ (a_|_ v b_|_))))
5		lea 152	. . . . 5 (a ^ b) =< a
6		lea 152	. . . . 5 (c ^ (a v b)) =< c
7	5, 6	le2an 161	. . . 4 ((a ^ b) ^ (c ^ (a v b))) =< (a ^ c)
8		lea 152	. . . . 5 (a_|_ ^ b_|_) =< a_|_
9		lea 152	. . . . 5 (c_|_ ^ (a_|_ v b_|_)) =< c_|_
10	8, 9	le2an 161	. . . 4 ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_))) =< (a_|_ ^ c_|_)
11	7, 10	le2or 160	. . 3 (((a ^ b) ^ (c ^ (a v b))) v ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_)))) =< ((a ^ c) v (a_|_ ^ c_|_))
12		leao1 154	. . . . . . . 8 (a ^ b) =< (a v b)
13		oran 79	. . . . . . . 8 (a v b) = (a_|_ ^ b_|_)_|_
14	12, 13	lbtr 131	. . . . . . 7 (a ^ b) =< (a_|_ ^ b_|_)_|_
15	14	lecom 172	. . . . . 6 (a ^ b) C (a_|_ ^ b_|_)_|_
16	15	comcom7 442	. . . . 5 (a ^ b) C (a_|_ ^ b_|_)
17		leor 151	. . . . . . . 8 (a ^ b) =< (c v (a ^ b))
18		df-a 39	. . . . . . . . . 10 (a ^ b) = (a_|_ v b_|_)_|_
19	18	lor 66	. . . . . . . . 9 (c v (a ^ b)) = (c v (a_|_ v b_|_)_|_)
20		oran1 83	. . . . . . . . 9 (c v (a_|_ v b_|_)_|_) = (c_|_ ^ (a_|_ v b_|_))_|_
21	19, 20	ax-r2 35	. . . . . . . 8 (c v (a ^ b)) = (c_|_ ^ (a_|_ v b_|_))_|_
22	17, 21	lbtr 131	. . . . . . 7 (a ^ b) =< (c_|_ ^ (a_|_ v b_|_))_|_
23	22	lecom 172	. . . . . 6 (a ^ b) C (c_|_ ^ (a_|_ v b_|_))_|_
24	23	comcom7 442	. . . . 5 (a ^ b) C (c_|_ ^ (a_|_ v b_|_))
25		lear 153	. . . . . . . 8 (c ^ (a v b)) =< (a v b)
26	25, 13	lbtr 131	. . . . . . 7 (c ^ (a v b)) =< (a_|_ ^ b_|_)_|_
27	26	lecom 172	. . . . . 6 (c ^ (a v b)) C (a_|_ ^ b_|_)_|_
28	27	comcom7 442	. . . . 5 (c ^ (a v b)) C (a_|_ ^ b_|_)
29		leao1 154	. . . . . . . 8 (c ^ (a v b)) =< (c v (a_|_ v b_|_)_|_)
30	29, 20	lbtr 131	. . . . . . 7 (c ^ (a v b)) =< (c_|_ ^ (a_|_ v b_|_))_|_
31	30	lecom 172	. . . . . 6 (c ^ (a v b)) C (c_|_ ^ (a_|_ v b_|_))_|_
32	31	comcom7 442	. . . . 5 (c ^ (a v b)) C (c_|_ ^ (a_|_ v b_|_))
33	16, 24, 28, 32	mh 861	. . . 4 (((a ^ b) v (a_|_ ^ b_|_)) ^ ((c ^ (a v b)) v (c_|_ ^ (a_|_ v b_|_)))) = ((((a ^ b) ^ (c ^ (a v b))) v ((a ^ b) ^ (c_|_ ^ (a_|_ v b_|_)))) v (((a_|_ ^ b_|_) ^ (c ^ (a v b))) v ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_)))))
34		an12 74	. . . . . . . 8 ((a ^ b) ^ (c_|_ ^ (a_|_ v b_|_))) = (c_|_ ^ ((a ^ b) ^ (a_|_ v b_|_)))
35		oran3 85	. . . . . . . . . . 11 (a_|_ v b_|_) = (a ^ b)_|_
36	35	lan 70	. . . . . . . . . 10 ((a ^ b) ^ (a_|_ v b_|_)) = ((a ^ b) ^ (a ^ b)_|_)
37		dff 93	. . . . . . . . . . 11 0 = ((a ^ b) ^ (a ^ b)_|_)
38	37	ax-r1 34	. . . . . . . . . 10 ((a ^ b) ^ (a ^ b)_|_) = 0
39	36, 38	ax-r2 35	. . . . . . . . 9 ((a ^ b) ^ (a_|_ v b_|_)) = 0
40	39	lan 70	. . . . . . . 8 (c_|_ ^ ((a ^ b) ^ (a_|_ v b_|_))) = (c_|_ ^ 0)
41		an0 100	. . . . . . . 8 (c_|_ ^ 0) = 0
42	34, 40, 41	3tr 62	. . . . . . 7 ((a ^ b) ^ (c_|_ ^ (a_|_ v b_|_))) = 0
43	42	lor 66	. . . . . 6 (((a ^ b) ^ (c ^ (a v b))) v ((a ^ b) ^ (c_|_ ^ (a_|_ v b_|_)))) = (((a ^ b) ^ (c ^ (a v b))) v 0)
44		or0 94	. . . . . 6 (((a ^ b) ^ (c ^ (a v b))) v 0) = ((a ^ b) ^ (c ^ (a v b)))
45	43, 44	ax-r2 35	. . . . 5 (((a ^ b) ^ (c ^ (a v b))) v ((a ^ b) ^ (c_|_ ^ (a_|_ v b_|_)))) = ((a ^ b) ^ (c ^ (a v b)))
46		an12 74	. . . . . . . 8 ((a_|_ ^ b_|_) ^ (c ^ (a v b))) = (c ^ ((a_|_ ^ b_|_) ^ (a v b)))
47	13	lan 70	. . . . . . . . . 10 ((a_|_ ^ b_|_) ^ (a v b)) = ((a_|_ ^ b_|_) ^ (a_|_ ^ b_|_)_|_)
48		dff 93	. . . . . . . . . . 11 0 = ((a_|_ ^ b_|_) ^ (a_|_ ^ b_|_)_|_)
49	48	ax-r1 34	. . . . . . . . . 10 ((a_|_ ^ b_|_) ^ (a_|_ ^ b_|_)_|_) = 0
50	47, 49	ax-r2 35	. . . . . . . . 9 ((a_|_ ^ b_|_) ^ (a v b)) = 0
51	50	lan 70	. . . . . . . 8 (c ^ ((a_|_ ^ b_|_) ^ (a v b))) = (c ^ 0)
52		an0 100	. . . . . . . 8 (c ^ 0) = 0
53	46, 51, 52	3tr 62	. . . . . . 7 ((a_|_ ^ b_|_) ^ (c ^ (a v b))) = 0
54	53	ax-r5 37	. . . . . 6 (((a_|_ ^ b_|_) ^ (c ^ (a v b))) v ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_)))) = (0 v ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_))))
55		or0r 95	. . . . . 6 (0 v ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_)))) = ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_)))
56	54, 55	ax-r2 35	. . . . 5 (((a_|_ ^ b_|_) ^ (c ^ (a v b))) v ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_)))) = ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_)))
57	45, 56	2or 67	. . . 4 ((((a ^ b) ^ (c ^ (a v b))) v ((a ^ b) ^ (c_|_ ^ (a_|_ v b_|_)))) v (((a_|_ ^ b_|_) ^ (c ^ (a v b))) v ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_))))) = (((a ^ b) ^ (c ^ (a v b))) v ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_))))
58	33, 57	ax-r2 35	. . 3 (((a ^ b) v (a_|_ ^ b_|_)) ^ ((c ^ (a v b)) v (c_|_ ^ (a_|_ v b_|_)))) = (((a ^ b) ^ (c ^ (a v b))) v ((a_|_ ^ b_|_) ^ (c_|_ ^ (a_|_ v b_|_))))
59		dfb 86	. . 3 (a == c) = ((a ^ c) v (a_|_ ^ c_|_))
60	11, 58, 59	le3tr1 132	. 2 (((a ^ b) v (a_|_ ^ b_|_)) ^ ((c ^ (a v b)) v (c_|_ ^ (a_|_ v b_|_)))) =< (a == c)
61	4, 60	letr 129	1 ((a == b) ^ ((a == c) v (b == c))) =< (a == c)

Syntax hints:   =< wle 2  _|_wn 4   == tb 5   v wo 6   ^ wa 7  0wf 10

This theorem is referenced by:  distid 869

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

metamath.org