Theorem orbi 824

Description: Disjunction of biconditionals.

Assertion

Ref	Expression
orbi	((a == c) v (b == c)) = (((a ->2 c) v (b ->2 c)) ^ ((c ->1 a) v (c ->1 b)))

Proof of Theorem orbi

Step	Hyp	Ref	Expression
1		dfb 86	. . 3 (a == c) = ((a ^ c) v (a_|_ ^ c_|_))
2		dfb 86	. . 3 (b == c) = ((b ^ c) v (b_|_ ^ c_|_))
3	1, 2	2or 67	. 2 ((a == c) v (b == c)) = (((a ^ c) v (a_|_ ^ c_|_)) v ((b ^ c) v (b_|_ ^ c_|_)))
4		ax-a2 30	. 2 (((a ^ c) v (a_|_ ^ c_|_)) v ((b ^ c) v (b_|_ ^ c_|_))) = (((b ^ c) v (b_|_ ^ c_|_)) v ((a ^ c) v (a_|_ ^ c_|_)))
5		ax-a3 31	. . 3 (((b ^ c) v (b_|_ ^ c_|_)) v ((a ^ c) v (a_|_ ^ c_|_))) = ((b ^ c) v ((b_|_ ^ c_|_) v ((a ^ c) v (a_|_ ^ c_|_))))
6		ancom 68	. . . . . . . 8 (a ^ c) = (c ^ a)
7	6	lor 66	. . . . . . 7 ((b_|_ ^ c_|_) v (a ^ c)) = ((b_|_ ^ c_|_) v (c ^ a))
8		imp3 823	. . . . . . . 8 ((b ->2 c) ^ (c ->1 a)) = ((b_|_ ^ c_|_) v (c ^ a))
9	8	ax-r1 34	. . . . . . 7 ((b_|_ ^ c_|_) v (c ^ a)) = ((b ->2 c) ^ (c ->1 a))
10	7, 9	ax-r2 35	. . . . . 6 ((b_|_ ^ c_|_) v (a ^ c)) = ((b ->2 c) ^ (c ->1 a))
11	10	ax-r5 37	. . . . 5 (((b_|_ ^ c_|_) v (a ^ c)) v (a_|_ ^ c_|_)) = (((b ->2 c) ^ (c ->1 a)) v (a_|_ ^ c_|_))
12		ax-a3 31	. . . . 5 (((b_|_ ^ c_|_) v (a ^ c)) v (a_|_ ^ c_|_)) = ((b_|_ ^ c_|_) v ((a ^ c) v (a_|_ ^ c_|_)))
13		df-i1 43	. . . . . . . 8 (c ->1 a) = (c_|_ v (c ^ a))
14		lear 153	. . . . . . . . . . 11 (a_|_ ^ c_|_) =< c_|_
15		leo 150	. . . . . . . . . . 11 c_|_ =< (c_|_ v (c ^ a))
16	14, 15	letr 129	. . . . . . . . . 10 (a_|_ ^ c_|_) =< (c_|_ v (c ^ a))
17	16	lecom 172	. . . . . . . . 9 (a_|_ ^ c_|_) C (c_|_ v (c ^ a))
18	17	comcom 435	. . . . . . . 8 (c_|_ v (c ^ a)) C (a_|_ ^ c_|_)
19	13, 18	bctr 173	. . . . . . 7 (c ->1 a) C (a_|_ ^ c_|_)
20		comi12 689	. . . . . . 7 (c ->1 a) C (b ->2 c)
21	19, 20	fh4rc 464	. . . . . 6 (((b ->2 c) ^ (c ->1 a)) v (a_|_ ^ c_|_)) = (((b ->2 c) v (a_|_ ^ c_|_)) ^ ((c ->1 a) v (a_|_ ^ c_|_)))
22	13	ax-r5 37	. . . . . . . 8 ((c ->1 a) v (a_|_ ^ c_|_)) = ((c_|_ v (c ^ a)) v (a_|_ ^ c_|_))
23		ax-a2 30	. . . . . . . 8 ((c_|_ v (c ^ a)) v (a_|_ ^ c_|_)) = ((a_|_ ^ c_|_) v (c_|_ v (c ^ a)))
24	16	df-le2 123	. . . . . . . 8 ((a_|_ ^ c_|_) v (c_|_ v (c ^ a))) = (c_|_ v (c ^ a))
25	22, 23, 24	3tr 62	. . . . . . 7 ((c ->1 a) v (a_|_ ^ c_|_)) = (c_|_ v (c ^ a))
26	25	lan 70	. . . . . 6 (((b ->2 c) v (a_|_ ^ c_|_)) ^ ((c ->1 a) v (a_|_ ^ c_|_))) = (((b ->2 c) v (a_|_ ^ c_|_)) ^ (c_|_ v (c ^ a)))
27	21, 26	ax-r2 35	. . . . 5 (((b ->2 c) ^ (c ->1 a)) v (a_|_ ^ c_|_)) = (((b ->2 c) v (a_|_ ^ c_|_)) ^ (c_|_ v (c ^ a)))
28	11, 12, 27	3tr2 61	. . . 4 ((b_|_ ^ c_|_) v ((a ^ c) v (a_|_ ^ c_|_))) = (((b ->2 c) v (a_|_ ^ c_|_)) ^ (c_|_ v (c ^ a)))
29	28	lor 66	. . 3 ((b ^ c) v ((b_|_ ^ c_|_) v ((a ^ c) v (a_|_ ^ c_|_)))) = ((b ^ c) v (((b ->2 c) v (a_|_ ^ c_|_)) ^ (c_|_ v (c ^ a))))
30		df-i2 44	. . . . . . . 8 (b ->2 c) = (c v (b_|_ ^ c_|_))
31	30	ax-r5 37	. . . . . . 7 ((b ->2 c) v (a_|_ ^ c_|_)) = ((c v (b_|_ ^ c_|_)) v (a_|_ ^ c_|_))
32		ax-a3 31	. . . . . . 7 ((c v (b_|_ ^ c_|_)) v (a_|_ ^ c_|_)) = (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_)))
33	31, 32	ax-r2 35	. . . . . 6 ((b ->2 c) v (a_|_ ^ c_|_)) = (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_)))
34		lear 153	. . . . . . . . 9 (b ^ c) =< c
35		leo 150	. . . . . . . . 9 c =< (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_)))
36	34, 35	letr 129	. . . . . . . 8 (b ^ c) =< (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_)))
37	36	lecom 172	. . . . . . 7 (b ^ c) C (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_)))
38	37	comcom 435	. . . . . 6 (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_))) C (b ^ c)
39	33, 38	bctr 173	. . . . 5 ((b ->2 c) v (a_|_ ^ c_|_)) C (b ^ c)
40		lea 152	. . . . . . . . . . 11 (c ^ (c ^ a)_|_) =< c
41	40, 35	letr 129	. . . . . . . . . 10 (c ^ (c ^ a)_|_) =< (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_)))
42	41	lecom 172	. . . . . . . . 9 (c ^ (c ^ a)_|_) C (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_)))
43	42	comcom 435	. . . . . . . 8 (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_))) C (c ^ (c ^ a)_|_)
44		anor1 80	. . . . . . . 8 (c ^ (c ^ a)_|_) = (c_|_ v (c ^ a))_|_
45	43, 44	cbtr 174	. . . . . . 7 (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_))) C (c_|_ v (c ^ a))_|_
46	45	comcom7 442	. . . . . 6 (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_))) C (c_|_ v (c ^ a))
47	33, 46	bctr 173	. . . . 5 ((b ->2 c) v (a_|_ ^ c_|_)) C (c_|_ v (c ^ a))
48	39, 47	fh4 454	. . . 4 ((b ^ c) v (((b ->2 c) v (a_|_ ^ c_|_)) ^ (c_|_ v (c ^ a)))) = (((b ^ c) v ((b ->2 c) v (a_|_ ^ c_|_))) ^ ((b ^ c) v (c_|_ v (c ^ a))))
49	30	lor 66	. . . . . . . 8 ((b ^ c) v (b ->2 c)) = ((b ^ c) v (c v (b_|_ ^ c_|_)))
50		leo 150	. . . . . . . . . 10 c =< (c v (b_|_ ^ c_|_))
51	34, 50	letr 129	. . . . . . . . 9 (b ^ c) =< (c v (b_|_ ^ c_|_))
52	51	df-le2 123	. . . . . . . 8 ((b ^ c) v (c v (b_|_ ^ c_|_))) = (c v (b_|_ ^ c_|_))
53	49, 52	ax-r2 35	. . . . . . 7 ((b ^ c) v (b ->2 c)) = (c v (b_|_ ^ c_|_))
54	53	ax-r5 37	. . . . . 6 (((b ^ c) v (b ->2 c)) v (a_|_ ^ c_|_)) = ((c v (b_|_ ^ c_|_)) v (a_|_ ^ c_|_))
55		ax-a3 31	. . . . . 6 (((b ^ c) v (b ->2 c)) v (a_|_ ^ c_|_)) = ((b ^ c) v ((b ->2 c) v (a_|_ ^ c_|_)))
56		ax-a2 30	. . . . . . . 8 ((c v (b_|_ ^ c_|_)) v (c v (a_|_ ^ c_|_))) = ((c v (a_|_ ^ c_|_)) v (c v (b_|_ ^ c_|_)))
57		orordi 104	. . . . . . . 8 (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_))) = ((c v (b_|_ ^ c_|_)) v (c v (a_|_ ^ c_|_)))
58		df-i2 44	. . . . . . . . 9 (a ->2 c) = (c v (a_|_ ^ c_|_))
59	58, 30	2or 67	. . . . . . . 8 ((a ->2 c) v (b ->2 c)) = ((c v (a_|_ ^ c_|_)) v (c v (b_|_ ^ c_|_)))
60	56, 57, 59	3tr1 60	. . . . . . 7 (c v ((b_|_ ^ c_|_) v (a_|_ ^ c_|_))) = ((a ->2 c) v (b ->2 c))
61	32, 60	ax-r2 35	. . . . . 6 ((c v (b_|_ ^ c_|_)) v (a_|_ ^ c_|_)) = ((a ->2 c) v (b ->2 c))
62	54, 55, 61	3tr2 61	. . . . 5 ((b ^ c) v ((b ->2 c) v (a_|_ ^ c_|_))) = ((a ->2 c) v (b ->2 c))
63		or12 73	. . . . . 6 ((b ^ c) v (c_|_