Theorem bi4 822

Description: Chained biconditional.

Assertion

Ref	Expression
bi4	(((a == b) ^ (b == c)) ^ (c == d)) = ((((a ^ b) ^ c) ^ d) v (((a_|_ ^ b_|_) ^ c_|_) ^ d_|_))

Proof of Theorem bi4

Step	Hyp	Ref	Expression
1		bi3 821	. . 3 ((a == b) ^ (b == c)) = (((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_))
2		u12lembi 708	. . . 4 ((c ->1 d) ^ (d ->2 c)) = (c == d)
3	2	ax-r1 34	. . 3 (c == d) = ((c ->1 d) ^ (d ->2 c))
4	1, 3	2an 72	. 2 (((a == b) ^ (b == c)) ^ (c == d)) = ((((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_)) ^ ((c ->1 d) ^ (d ->2 c)))
5		df-i1 43	. . . . . 6 (c ->1 d) = (c_|_ v (c ^ d))
6	5	lan 70	. . . . 5 ((((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_)) ^ (c ->1 d)) = ((((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_)) ^ (c_|_ v (c ^ d)))
7		leao2 155	. . . . . . 7 ((a_|_ ^ b_|_) ^ c_|_) =< (c_|_ v (c ^ d))
8	7	lecom 172	. . . . . 6 ((a_|_ ^ b_|_) ^ c_|_) C (c_|_ v (c ^ d))
9		leao4 157	. . . . . . . . . 10 ((a ^ b) ^ c) =< ((a_|_ ^ b_|_)_|_ v c)
10		oran2 84	. . . . . . . . . 10 ((a_|_ ^ b_|_)_|_ v c) = ((a_|_ ^ b_|_) ^ c_|_)_|_
11	9, 10	lbtr 131	. . . . . . . . 9 ((a ^ b) ^ c) =< ((a_|_ ^ b_|_) ^ c_|_)_|_
12	11	lecom 172	. . . . . . . 8 ((a ^ b) ^ c) C ((a_|_ ^ b_|_) ^ c_|_)_|_
13	12	comcom 435	. . . . . . 7 ((a_|_ ^ b_|_) ^ c_|_)_|_ C ((a ^ b) ^ c)
14	13	comcom6 441	. . . . . 6 ((a_|_ ^ b_|_) ^ c_|_) C ((a ^ b) ^ c)
15	8, 14	fh2rc 462	. . . . 5 ((((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_)) ^ (c_|_ v (c ^ d))) = ((((a ^ b) ^ c) ^ (c_|_ v (c ^ d))) v (((a_|_ ^ b_|_) ^ c_|_) ^ (c_|_ v (c ^ d))))
16		comanr2 447	. . . . . . . . 9 c C ((a ^ b) ^ c)
17	16	comcom3 436	. . . . . . . 8 c_|_ C ((a ^ b) ^ c)
18		comanr1 446	. . . . . . . . 9 c C (c ^ d)
19	18	comcom3 436	. . . . . . . 8 c_|_ C (c ^ d)
20	17, 19	fh2 452	. . . . . . 7 (((a ^ b) ^ c) ^ (c_|_ v (c ^ d))) = ((((a ^ b) ^ c) ^ c_|_) v (((a ^ b) ^ c) ^ (c ^ d)))
21		anass 69	. . . . . . . . 9 (((a ^ b) ^ c) ^ c_|_) = ((a ^ b) ^ (c ^ c_|_))
22		dff 93	. . . . . . . . . . 11 0 = (c ^ c_|_)
23	22	lan 70	. . . . . . . . . 10 ((a ^ b) ^ 0) = ((a ^ b) ^ (c ^ c_|_))
24	23	ax-r1 34	. . . . . . . . 9 ((a ^ b) ^ (c ^ c_|_)) = ((a ^ b) ^ 0)
25		an0 100	. . . . . . . . 9 ((a ^ b) ^ 0) = 0
26	21, 24, 25	3tr 62	. . . . . . . 8 (((a ^ b) ^ c) ^ c_|_) = 0
27		anass 69	. . . . . . . . . 10 ((((a ^ b) ^ c) ^ c) ^ d) = (((a ^ b) ^ c) ^ (c ^ d))
28	27	ax-r1 34	. . . . . . . . 9 (((a ^ b) ^ c) ^ (c ^ d)) = ((((a ^ b) ^ c) ^ c) ^ d)
29		anass 69	. . . . . . . . . . 11 (((a ^ b) ^ c) ^ c) = ((a ^ b) ^ (c ^ c))
30		anidm 103	. . . . . . . . . . . 12 (c ^ c) = c
31	30	lan 70	. . . . . . . . . . 11 ((a ^ b) ^ (c ^ c)) = ((a ^ b) ^ c)
32	29, 31	ax-r2 35	. . . . . . . . . 10 (((a ^ b) ^ c) ^ c) = ((a ^ b) ^ c)
33	32	ran 71	. . . . . . . . 9 ((((a ^ b) ^ c) ^ c) ^ d) = (((a ^ b) ^ c) ^ d)
34	28, 33	ax-r2 35	. . . . . . . 8 (((a ^ b) ^ c) ^ (c ^ d)) = (((a ^ b) ^ c) ^ d)
35	26, 34	2or 67	. . . . . . 7 ((((a ^ b) ^ c) ^ c_|_) v (((a ^ b) ^ c) ^ (c ^ d))) = (0 v (((a ^ b) ^ c) ^ d))
36		or0r 95	. . . . . . 7 (0 v (((a ^ b) ^ c) ^ d)) = (((a ^ b) ^ c) ^ d)
37	20, 35, 36	3tr 62	. . . . . 6 (((a ^ b) ^ c) ^ (c_|_ v (c ^ d))) = (((a ^ b) ^ c) ^ d)
38		comanr2 447	. . . . . . . 8 c_|_ C ((a_|_ ^ b_|_) ^ c_|_)
39	38, 19	fh2 452	. . . . . . 7 (((a_|_ ^ b_|_) ^ c_|_) ^ (c_|_ v (c ^ d))) = ((((a_|_ ^ b_|_) ^ c_|_) ^ c_|_) v (((a_|_ ^ b_|_) ^ c_|_) ^ (c ^ d)))
40		anass 69	. . . . . . . . 9 (((a_|_ ^ b_|_) ^ c_|_) ^ c_|_) = ((a_|_ ^ b_|_) ^ (c_|_ ^ c_|_))
41		anidm 103	. . . . . . . . . 10 (c_|_ ^ c_|_) = c_|_
42	41	lan 70	. . . . . . . . 9 ((a_|_ ^ b_|_) ^ (c_|_ ^ c_|_)) = ((a_|_ ^ b_|_) ^ c_|_)
43	40, 42	ax-r2 35	. . . . . . . 8 (((a_|_ ^ b_|_) ^ c_|_) ^ c_|_) = ((a_|_ ^ b_|_) ^ c_|_)
44		an4 78	. . . . . . . . 9 (((a_|_ ^ b_|_) ^ c_|_) ^ (c ^ d)) = (((a_|_ ^ b_|_) ^ c) ^ (c_|_ ^ d))
45		anass 69	. . . . . . . . 9 (((a_|_ ^ b_|_) ^ c) ^ (c_|_ ^ d)) = ((a_|_ ^ b_|_) ^ (c ^ (c_|_ ^ d)))
46	22	ran 71	. . . . . . . . . . . . 13 (0 ^ d) = ((c ^ c_|_) ^ d)
47	46	ax-r1 34	. . . . . . . . . . . 12 ((c ^ c_|_) ^ d) = (0 ^ d)
48		anass 69	. . . . . . . . . . . 12 ((c ^ c_|_) ^ d) = (c ^ (c_|_ ^ d))
49		an0r 101	. . . . . . . . . . . 12 (0 ^ d) = 0
50	47, 48, 49	3tr2 61	. . . . . . . . . . 11 (c ^ (c_|_ ^ d)) = 0
51	50	lan 70	. . . . . . . . . 10 ((a_|_ ^ b_|_) ^ (c ^ (c_|_ ^ d))) = ((a_|_ ^ b_|_) ^ 0)
52		an0 100	. . . . . . . . . 10 ((a_|_ ^ b_|_) ^ 0) = 0
53	51, 52	ax-r2 35	. . . . . . . . 9 ((a_|_ ^ b_|_) ^ (c ^ (c_|_ ^ d))) = 0
54	44, 45, 53	3tr 62	. . . . . . . 8 (((a_|_ ^ b_|_) ^ c_|_) ^ (c ^ d)) = 0
55	43, 54	2or 67	. . . . . . 7 ((((a_|_ ^ b_|_) ^ c_|_) ^ c_|_) v (((a_|_ ^ b_|_) ^ c_|_) ^ (c ^ d))) = (((a_|_ ^ b_|_) ^ c_|_) v 0)
56		or0 94	. . . . . . 7 (((a_|_ ^ b_|_) ^ c_|_) v 0) = ((a_|_ ^ b_|_) ^ c_|_)
57	39, 55, 56	3tr 62	. . . . . 6 (((a_|_ ^ b_|_) ^ c_|_) ^ (c_|_ v (c ^ d))) = ((a_|_ ^ b_|_) ^ c_|_)
58	37, 57	2or 67	. . . . 5 ((((a ^ b) ^ c) ^ (c_|_ v (c ^ d))) v (((a_|_ ^ b_|_) ^ c_|_) ^ (c_|_ v (c ^ d)))) = ((((a ^ b) ^ c) ^ d) v ((a_|_ ^ b_|_) ^ c_|_))
59	6, 15, 58	3tr 62	. . . 4 ((((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_)) ^ (c ->1 d)) = ((((a ^ b) ^ c) ^ d) v ((a_|_ ^ b_|_) ^ c_|_))
60	59	ran 71	. . 3 (((((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_)) ^ (c ->1 d)) ^ (d ->2 c)) = (((((a ^ b) ^ c) ^ d) v ((a_|_ ^ b_|_) ^ c_|_)) ^ (d ->2 c))
61		anass 69	. . 3 (((((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_)) ^ (c ->1 d)) ^ (d ->2 c)) = ((((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_)) ^ ((c ->1 d) ^ (d ->2 c)))
62		anass 69	. . . . . . . 8 ((((a ^ b) ^ c) ^ d) ^ (d ->2 c)) = (((a ^ b) ^ c) ^ (d ^ (d ->2 c)))
63		an4 78	. . . . . . . 8 (((a ^ b) ^ c) ^ (d ^ (d ->2 c))) = (((a ^ b) ^ d) ^ (c ^ (d ->2 c)))
64		ancom 68	. . . . . . . . . . 11 (c ^ (d ->2 c)) = ((d ->2 c) ^ c)
65		u2lemab 593	. . . . . . . . . . 11 ((d ->2 c) ^ c) = c
66	64, 65	ax-r2 35	. . . . . . . . . 10 (c ^ (d ->2 c)) = c
67	66	lan 70	. . . . . . . . 9 (((a ^ b) ^ d) ^ (c ^ (d ->2