Theorem bi3 821

Description: Chained biconditional.

Assertion

Ref	Expression
bi3	((a == b) ^ (b == c)) = (((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_))

Proof of Theorem bi3

Step	Hyp	Ref	Expression
1		dfb 86	. . 3 (a == b) = ((a ^ b) v (a_|_ ^ b_|_))
2		u12lembi 708	. . . 4 ((b ->1 c) ^ (c ->2 b)) = (b == c)
3	2	ax-r1 34	. . 3 (b == c) = ((b ->1 c) ^ (c ->2 b))
4	1, 3	2an 72	. 2 ((a == b) ^ (b == c)) = (((a ^ b) v (a_|_ ^ b_|_)) ^ ((b ->1 c) ^ (c ->2 b)))
5		df-i1 43	. . . . . 6 (b ->1 c) = (b_|_ v (b ^ c))
6	5	lan 70	. . . . 5 (((a ^ b) v (a_|_ ^ b_|_)) ^ (b ->1 c)) = (((a ^ b) v (a_|_ ^ b_|_)) ^ (b_|_ v (b ^ c)))
7		lear 153	. . . . . . . 8 (a_|_ ^ b_|_) =< b_|_
8		leo 150	. . . . . . . 8 b_|_ =< (b_|_ v (b ^ c))
9	7, 8	letr 129	. . . . . . 7 (a_|_ ^ b_|_) =< (b_|_ v (b ^ c))
10	9	lecom 172	. . . . . 6 (a_|_ ^ b_|_) C (b_|_ v (b ^ c))
11		coman1 177	. . . . . . . 8 (a_|_ ^ b_|_) C a_|_
12	11	comcom7 442	. . . . . . 7 (a_|_ ^ b_|_) C a
13		coman2 178	. . . . . . . 8 (a_|_ ^ b_|_) C b_|_
14	13	comcom7 442	. . . . . . 7 (a_|_ ^ b_|_) C b
15	12, 14	com2an 466	. . . . . 6 (a_|_ ^ b_|_) C (a ^ b)
16	10, 15	fh2rc 462	. . . . 5 (((a ^ b) v (a_|_ ^ b_|_)) ^ (b_|_ v (b ^ c))) = (((a ^ b) ^ (b_|_ v (b ^ c))) v ((a_|_ ^ b_|_) ^ (b_|_ v (b ^ c))))
17		comanr2 447	. . . . . . . . 9 b C (a ^ b)
18	17	comcom3 436	. . . . . . . 8 b_|_ C (a ^ b)
19		comanr1 446	. . . . . . . . 9 b C (b ^ c)
20	19	comcom3 436	. . . . . . . 8 b_|_ C (b ^ c)
21	18, 20	fh2 452	. . . . . . 7 ((a ^ b) ^ (b_|_ v (b ^ c))) = (((a ^ b) ^ b_|_) v ((a ^ b) ^ (b ^ c)))
22		anass 69	. . . . . . . . 9 ((a ^ b) ^ b_|_) = (a ^ (b ^ b_|_))
23		dff 93	. . . . . . . . . . 11 0 = (b ^ b_|_)
24	23	lan 70	. . . . . . . . . 10 (a ^ 0) = (a ^ (b ^ b_|_))
25	24	ax-r1 34	. . . . . . . . 9 (a ^ (b ^ b_|_)) = (a ^ 0)
26		an0 100	. . . . . . . . 9 (a ^ 0) = 0
27	22, 25, 26	3tr 62	. . . . . . . 8 ((a ^ b) ^ b_|_) = 0
28		anass 69	. . . . . . . . . 10 (((a ^ b) ^ b) ^ c) = ((a ^ b) ^ (b ^ c))
29	28	ax-r1 34	. . . . . . . . 9 ((a ^ b) ^ (b ^ c)) = (((a ^ b) ^ b) ^ c)
30		anass 69	. . . . . . . . . . 11 ((a ^ b) ^ b) = (a ^ (b ^ b))
31		anidm 103	. . . . . . . . . . . 12 (b ^ b) = b
32	31	lan 70	. . . . . . . . . . 11 (a ^ (b ^ b)) = (a ^ b)
33	30, 32	ax-r2 35	. . . . . . . . . 10 ((a ^ b) ^ b) = (a ^ b)
34	33	ran 71	. . . . . . . . 9 (((a ^ b) ^ b) ^ c) = ((a ^ b) ^ c)
35	29, 34	ax-r2 35	. . . . . . . 8 ((a ^ b) ^ (b ^ c)) = ((a ^ b) ^ c)
36	27, 35	2or 67	. . . . . . 7 (((a ^ b) ^ b_|_) v ((a ^ b) ^ (b ^ c))) = (0 v ((a ^ b) ^ c))
37		or0r 95	. . . . . . 7 (0 v ((a ^ b) ^ c)) = ((a ^ b) ^ c)
38	21, 36, 37	3tr 62	. . . . . 6 ((a ^ b) ^ (b_|_ v (b ^ c))) = ((a ^ b) ^ c)
39	13	comcom 435	. . . . . . . 8 b_|_ C (a_|_ ^ b_|_)
40	39, 20	fh2 452	. . . . . . 7 ((a_|_ ^ b_|_) ^ (b_|_ v (b ^ c))) = (((a_|_ ^ b_|_) ^ b_|_) v ((a_|_ ^ b_|_) ^ (b ^ c)))
41		anass 69	. . . . . . . . 9 ((a_|_ ^ b_|_) ^ b_|_) = (a_|_ ^ (b_|_ ^ b_|_))
42		anidm 103	. . . . . . . . . 10 (b_|_ ^ b_|_) = b_|_
43	42	lan 70	. . . . . . . . 9 (a_|_ ^ (b_|_ ^ b_|_)) = (a_|_ ^ b_|_)
44	41, 43	ax-r2 35	. . . . . . . 8 ((a_|_ ^ b_|_) ^ b_|_) = (a_|_ ^ b_|_)
45		an4 78	. . . . . . . . 9 ((a_|_ ^ b_|_) ^ (b ^ c)) = ((a_|_ ^ b) ^ (b_|_ ^ c))
46		anass 69	. . . . . . . . 9 ((a_|_ ^ b) ^ (b_|_ ^ c)) = (a_|_ ^ (b ^ (b_|_ ^ c)))
47	23	ran 71	. . . . . . . . . . . . 13 (0 ^ c) = ((b ^ b_|_) ^ c)
48	47	ax-r1 34	. . . . . . . . . . . 12 ((b ^ b_|_) ^ c) = (0 ^ c)
49		anass 69	. . . . . . . . . . . 12 ((b ^ b_|_) ^ c) = (b ^ (b_|_ ^ c))
50		an0r 101	. . . . . . . . . . . 12 (0 ^ c) = 0
51	48, 49, 50	3tr2 61	. . . . . . . . . . 11 (b ^ (b_|_ ^ c)) = 0
52	51	lan 70	. . . . . . . . . 10 (a_|_ ^ (b ^ (b_|_ ^ c))) = (a_|_ ^ 0)
53		an0 100	. . . . . . . . . 10 (a_|_ ^ 0) = 0
54	52, 53	ax-r2 35	. . . . . . . . 9 (a_|_ ^ (b ^ (b_|_ ^ c))) = 0
55	45, 46, 54	3tr 62	. . . . . . . 8 ((a_|_ ^ b_|_) ^ (b ^ c)) = 0
56	44, 55	2or 67	. . . . . . 7 (((a_|_ ^ b_|_) ^ b_|_) v ((a_|_ ^ b_|_) ^ (b ^ c))) = ((a_|_ ^ b_|_) v 0)
57		or0 94	. . . . . . 7 ((a_|_ ^ b_|_) v 0) = (a_|_ ^ b_|_)
58	40, 56, 57	3tr 62	. . . . . 6 ((a_|_ ^ b_|_) ^ (b_|_ v (b ^ c))) = (a_|_ ^ b_|_)
59	38, 58	2or 67	. . . . 5 (((a ^ b) ^ (b_|_ v (b ^ c))) v ((a_|_ ^ b_|_) ^ (b_|_ v (b ^ c)))) = (((a ^ b) ^ c) v (a_|_ ^ b_|_))
60	6, 16, 59	3tr 62	. . . 4 (((a ^ b) v (a_|_ ^ b_|_)) ^ (b ->1 c)) = (((a ^ b) ^ c) v (a_|_ ^ b_|_))
61	60	ran 71	. . 3 ((((a ^ b) v (a_|_ ^ b_|_)) ^ (b ->1 c)) ^ (c ->2 b)) = ((((a ^ b) ^ c) v (a_|_ ^ b_|_)) ^ (c ->2 b))
62		anass 69	. . 3 ((((a ^ b) v (a_|_ ^ b_|_)) ^ (b ->1 c)) ^ (c ->2 b)) = (((a ^ b) v (a_|_ ^ b_|_)) ^ ((b ->1 c) ^ (c ->2 b)))
63		lear 153	. . . . . . . 8 ((a ^ c) ^ b) =< b
64		leo 150	. . . . . . . 8 b =< (b v (c_|_ ^ b_|_))
65	63, 64	letr 129	. . . . . . 7 ((a ^ c) ^ b) =< (b v (c_|_ ^ b_|_))
66		an32 76	. . . . . . 7 ((a ^ b) ^ c) = ((a ^ c) ^ b)
67		df-i2 44	. . . . . . 7 (c ->2 b) = (b v (c_|_ ^ b_|_))
68	65, 66, 67	le3tr1 132	. . . . . 6 ((a ^ b) ^ c) =< (c ->2 b)
69	68	lecom 172	. . . . 5 ((a ^ b) ^ c) C (c ->2 b)
70		anass 69	. . . . . . . . . 10 ((a ^ b) ^ c) = (a ^ (b ^ c))
71		lea 152	. . . . . . . . . 10 (a ^ (b ^ c)) =< a
72	70, 71	bltr 130	. . . . . . . . 9 ((a ^ b) ^ c) =< a
73		leo 150	. . . . . . . . 9 a =< (a v b)
74	72, 73	letr 129	. . . . . . . 8 ((a ^ b) ^ c) =< (a v b)
75		oran 79	. . . . . . . 8 (a v b) = (a_|_ ^ b_|_)_|_
76	74, 75	lbtr 131	. . . . . . 7 ((a ^ b) ^ c) =< (a_|_ ^ b_|_)_|_
77	76	lecom 172	. . . . . 6 ((a ^ b) ^ c) C (a_|_ ^ b_|_)_|_
78	77	comcom7 442	. . . . 5 ((a ^ b) ^ c) C (a_|_ ^ b_|_)
79	69, 78	fh2r 456	. . . 4 ((((a ^ b) ^ c) v (a_|_ ^ b_|_)) ^ (c ->2 b)) = ((((a ^ b) ^ c) ^ (c ->2 b)) v ((a_|_ ^ b_|_) ^ (c ->2 b)))
80		anass 69	. . . . . 6 (((a ^ b) ^ c) ^ (c ->2 b)) = ((a ^ b) ^ (c ^ (c ->2 b)))
81		an4 78	. . . . . 6 ((a ^ b) ^ (c ^ (c ->2 b))) = ((a ^ c) ^ (b ^ (c ->2 b)))
82		ancom 68	. . . . . . . . 9 (b ^ (c ->2 b)) = ((c ->2 b) ^ b)
83		u2lemab 593	. . . . . . . . 9 ((c ->2 b) ^ b) = b
84	82, 83	ax-r2 35	. . . . . . . 8 (b ^ (c ->2 b)) = b
85	84	lan 70	. . . . . . 7 ((a ^ c) ^ (b ^ (c ->2 b))) = ((a ^ c) ^ b)
86		an32 76	. . . . . . 7 ((a ^ c) ^ b) = ((a ^ b) ^ c)
87	85, 86	ax-r2 35	. . . . . 6 ((a ^ c) ^ (b ^ (c ->2 b))) = ((a ^ b) ^ c)
88	80, 81, 87	3tr 62	. . . . 5 (((a ^ b) ^ c) ^ (c ->2 b)) = ((a ^ b) ^ c)
89		anass 69	. . . . . 6 ((a_|_ ^ b_|_) ^ (c ->2 b)) = (a_|_ ^ (b_|_ ^ (c ->2 b)))
90		ancom 68	. . . . . . . 8 (b_|_ ^ (c ->2 b)) = ((c ->2 b) ^ b_|_)
91		u2lemanb 598