Theorem mlaoml 815

Description: Mladen's OML.

Assertion

Ref	Expression
mlaoml	((a == b) ^ (b == c)) =< (a == c)

Proof of Theorem mlaoml

Step	Hyp	Ref	Expression
1		u1lembi 702	. . . . 5 ((a ->1 b) ^ (b ->1 a)) = (a == b)
2	1	ran 71	. . . 4 (((a ->1 b) ^ (b ->1 a)) ^ (b ->1 c)) = ((a == b) ^ (b ->1 c))
3		mlalem 814	. . . 4 ((a == b) ^ (b ->1 c)) =< (a ->1 c)
4	2, 3	bltr 130	. . 3 (((a ->1 b) ^ (b ->1 a)) ^ (b ->1 c)) =< (a ->1 c)
5		ancom 68	. . . . . 6 ((b ->1 a) ^ (c ->1 b)) = ((c ->1 b) ^ (b ->1 a))
6	5	ran 71	. . . . 5 (((b ->1 a) ^ (c ->1 b)) ^ (b ->1 c)) = (((c ->1 b) ^ (b ->1 a)) ^ (b ->1 c))
7		an32 76	. . . . 5 (((c ->1 b) ^ (b ->1 a)) ^ (b ->1 c)) = (((c ->1 b) ^ (b ->1 c)) ^ (b ->1 a))
8		u1lembi 702	. . . . . 6 ((c ->1 b) ^ (b ->1 c)) = (c == b)
9	8	ran 71	. . . . 5 (((c ->1 b) ^ (b ->1 c)) ^ (b ->1 a)) = ((c == b) ^ (b ->1 a))
10	6, 7, 9	3tr 62	. . . 4 (((b ->1 a) ^ (c ->1 b)) ^ (b ->1 c)) = ((c == b) ^ (b ->1 a))
11		mlalem 814	. . . 4 ((c == b) ^ (b ->1 a)) =< (c ->1 a)
12	10, 11	bltr 130	. . 3 (((b ->1 a) ^ (c ->1 b)) ^ (b ->1 c)) =< (c ->1 a)
13	4, 12	le2an 161	. 2 ((((a ->1 b) ^ (b ->1 a)) ^ (b ->1 c)) ^ (((b ->1 a) ^ (c ->1 b)) ^ (b ->1 c))) =< ((a ->1 c) ^ (c ->1 a))
14		an12 74	. . . . . 6 ((b ->1 a) ^ ((a ->1 b) ^ (c ->1 b))) = ((a ->1 b) ^ ((b ->1 a) ^ (c ->1 b)))
15		ancom 68	. . . . . . . 8 ((a ->1 b) ^ (b ->1 a)) = ((b ->1 a) ^ (a ->1 b))
16	15	ran 71	. . . . . . 7 (((a ->1 b) ^ (b ->1 a)) ^ ((b ->1 a) ^ (c ->1 b))) = (((b ->1 a) ^ (a ->1 b)) ^ ((b ->1 a) ^ (c ->1 b)))
17		id 58	. . . . . . 7 (((a ->1 b) ^ (b ->1 a)) ^ ((b ->1 a) ^ (c ->1 b))) = (((a ->1 b) ^ (b ->1 a)) ^ ((b ->1 a) ^ (c ->1 b)))
18		anandi 106	. . . . . . 7 ((b ->1 a) ^ ((a ->1 b) ^ (c ->1 b))) = (((b ->1 a) ^ (a ->1 b)) ^ ((b ->1 a) ^ (c ->1 b)))
19	16, 17, 18	3tr1 60	. . . . . 6 (((a ->1 b) ^ (b ->1 a)) ^ ((b ->1 a) ^ (c ->1 b))) = ((b ->1 a) ^ ((a ->1 b) ^ (c ->1 b)))
20		anass 69	. . . . . 6 (((a ->1 b) ^ (b ->1 a)) ^ (c ->1 b)) = ((a ->1 b) ^ ((b ->1 a) ^ (c ->1 b)))
21	14, 19, 20	3tr1 60	. . . . 5 (((a ->1 b) ^ (b ->1 a)) ^ ((b ->1 a) ^ (c ->1 b))) = (((a ->1 b) ^ (b ->1 a)) ^ (c ->1 b))
22	21	ran 71	. . . 4 ((((a ->1 b) ^ (b ->1 a)) ^ ((b ->1 a) ^ (c ->1 b))) ^ (b ->1 c)) = ((((a ->1 b) ^ (b ->1 a)) ^ (c ->1 b)) ^ (b ->1 c))
23		anandir 107	. . . 4 ((((a ->1 b) ^ (b ->1 a)) ^ ((b ->1 a) ^ (c ->1 b))) ^ (b ->1 c)) = ((((a ->1 b) ^ (b ->1 a)) ^ (b ->1 c)) ^ (((b ->1 a) ^ (c ->1 b)) ^ (b ->1 c)))
24		an32 76	. . . 4 ((((a ->1 b) ^ (b ->1 a)) ^ (c ->1 b)) ^ (b ->1 c)) = ((((a ->1 b) ^ (b ->1 a)) ^ (b ->1 c)) ^ (c ->1 b))
25	22, 23, 24	3tr2 61	. . 3 ((((a ->1 b) ^ (b ->1 a)) ^ (b ->1 c)) ^ (((b ->1 a) ^ (c ->1 b)) ^ (b ->1 c))) = ((((a ->1 b) ^ (b ->1 a)) ^ (b ->1 c)) ^ (c ->1 b))
26		anass 69	. . 3 ((((a ->1 b) ^ (b ->1 a)) ^ (b ->1 c)) ^ (c ->1 b)) = (((a ->1 b) ^ (b ->1 a)) ^ ((b ->1 c) ^ (c ->1 b)))
27		u1lembi 702	. . . 4 ((b ->1 c) ^ (c ->1 b)) = (b == c)
28	1, 27	2an 72	. . 3 (((a ->1 b) ^ (b ->1 a)) ^ ((b ->1 c) ^ (c ->1 b))) = ((a == b) ^ (b == c))
29	25, 26, 28	3tr 62	. 2 ((((a ->1 b) ^ (b ->1 a)) ^ (b ->1 c)) ^ (((b ->1 a) ^ (c ->1 b)) ^ (b ->1 c))) = ((a == b) ^ (b == c))
30		u1lembi 702	. 2 ((a ->1 c) ^ (c ->1 a)) = (a == c)
31	13, 29, 30	le3tr2 133	1 ((a == b) ^ (b == c)) =< (a == c)

Syntax hints:   =< wle 2   == tb 5   ^ wa 7   ->1 wi1 13

This theorem is referenced by:  eqtr4 816  mlaconj4 826

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