Theorem test 784

Description: Part of an attempt to crack a potential Kalmbach axiom.

Assertion

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

Proof of Theorem test

Step	Hyp	Ref	Expression
1		oran3 85	. . . . 5 (a_|_ v b_|_) = (a ^ b)_|_
2	1	lor 66	. . . 4 (c v (a_|_ v b_|_)) = (c v (a ^ b)_|_)
3	2	ran 71	. . 3 ((c v (a_|_ v b_|_)) ^ (c_|_ ^ (c v (a ^ b)))) = ((c v (a ^ b)_|_) ^ (c_|_ ^ (c v (a ^ b))))
4	3	ax-r5 37	. 2 (((c v (a_|_ v b_|_)) ^ (c_|_ ^ (c v (a ^ b)))) v ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b))))) = (((c v (a ^ b)_|_) ^ (c_|_ ^ (c v (a ^ b)))) v ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b)))))
5		comor1 443	. . . . . . 7 (c v (a ^ b)_|_) C c
6	5	comcom2 175	. . . . . 6 (c v (a ^ b)_|_) C c_|_
7		comor2 444	. . . . . . 7 (c v (a ^ b)_|_) C (a ^ b)_|_
8	7	comcom7 442	. . . . . 6 (c v (a ^ b)_|_) C (a ^ b)
9	6, 8	com2an 466	. . . . 5 (c v (a ^ b)_|_) C (c_|_ ^ (a ^ b))
10	6, 8	com2or 465	. . . . . 6 (c v (a ^ b)_|_) C (c_|_ v (a ^ b))
11	5, 10	com2an 466	. . . . 5 (c v (a ^ b)_|_) C (c ^ (c_|_ v (a ^ b)))
12	9, 11	com2or 465	. . . 4 (c v (a ^ b)_|_) C ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b))))
13	5, 8	com2or 465	. . . . 5 (c v (a ^ b)_|_) C (c v (a ^ b))
14	6, 13	com2an 466	. . . 4 (c v (a ^ b)_|_) C (c_|_ ^ (c v (a ^ b)))
15	12, 14	fh4r 458	. . 3 (((c v (a ^ b)_|_) ^ (c_|_ ^ (c v (a ^ b)))) v ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b))))) = (((c v (a ^ b)_|_) v ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b))))) ^ ((c_|_ ^ (c v (a ^ b))) v ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b))))))
16		ax-a3 31	. . . . . . 7 (((c v (a ^ b)_|_) v (c_|_ ^ (a ^ b))) v (c ^ (c_|_ v (a ^ b)))) = ((c v (a ^ b)_|_) v ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b)))))
17	16	ax-r1 34	. . . . . 6 ((c v (a ^ b)_|_) v ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b))))) = (((c v (a ^ b)_|_) v (c_|_ ^ (a ^ b))) v (c ^ (c_|_ v (a ^ b))))
18		ax-a2 30	. . . . . . 7 (((c v (a ^ b)_|_) v (c_|_ ^ (a ^ b))) v (c ^ (c_|_ v (a ^ b)))) = ((c ^ (c_|_ v (a ^ b))) v ((c v (a ^ b)_|_) v (c_|_ ^ (a ^ b))))
19		anor2 81	. . . . . . . . . . 11 (c_|_ ^ (a ^ b)) = (c v (a ^ b)_|_)_|_
20	19	lor 66	. . . . . . . . . 10 ((c v (a ^ b)_|_) v (c_|_ ^ (a ^ b))) = ((c v (a ^ b)_|_) v (c v (a ^ b)_|_)_|_)
21		df-t 40	. . . . . . . . . . 11 1 = ((c v (a ^ b)_|_) v (c v (a ^ b)_|_)_|_)
22	21	ax-r1 34	. . . . . . . . . 10 ((c v (a ^ b)_|_) v (c v (a ^ b)_|_)_|_) = 1
23	20, 22	ax-r2 35	. . . . . . . . 9 ((c v (a ^ b)_|_) v (c_|_ ^ (a ^ b))) = 1
24	23	lor 66	. . . . . . . 8 ((c ^ (c_|_ v (a ^ b))) v ((c v (a ^ b)_|_) v (c_|_ ^ (a ^ b)))) = ((c ^ (c_|_ v (a ^ b))) v 1)
25		or1 96	. . . . . . . 8 ((c ^ (c_|_ v (a ^ b))) v 1) = 1
26	24, 25	ax-r2 35	. . . . . . 7 ((c ^ (c_|_ v (a ^ b))) v ((c v (a ^ b)_|_) v (c_|_ ^ (a ^ b)))) = 1
27	18, 26	ax-r2 35	. . . . . 6 (((c v (a ^ b)_|_) v (c_|_ ^ (a ^ b))) v (c ^ (c_|_ v (a ^ b)))) = 1
28	17, 27	ax-r2 35	. . . . 5 ((c v (a ^ b)_|_) v ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b))))) = 1
29		ax-a3 31	. . . . . . 7 (((c_|_ ^ (c v (a ^ b))) v (c_|_ ^ (a ^ b))) v (c ^ (c_|_ v (a ^ b)))) = ((c_|_ ^ (c v (a ^ b))) v ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b)))))
30	29	ax-r1 34	. . . . . 6 ((c_|_ ^ (c v (a ^ b))) v ((c_|_ ^ (a ^ b)) v (c ^ (c_|_ v (a ^ b))))) = (((c_|_ ^ (c v (a ^ b))) v (c_|_ ^ (a ^ b))) v (c ^ (c_|_ v (a ^ b))))
31		ax-a2 30	. . . . . . . . 9 ((c_|_ ^ (c v (a ^ b))) v (c_|_ ^ (a ^ b))) = ((c_|_ ^ (a ^ b)) v (c_|_ ^ (c v (a ^ b))))
32		leor 151	. . . . . . . . . . 11 (a ^ b) =< (c v (a ^ b))
33	32	lelan 159	. . . . . . . . . 10 (c_|_ ^ (a ^ b)) =< (c_|_ ^ (c v (a ^ b)))
34	33	df-le2 123	. . . . . . . . 9 ((c_|_ ^ (a ^ b)) v (c_|_ ^ (c v (a ^ b)))) = (c_|_ ^ (c v (a ^ b)))
35	31, 34	ax-r2 35	. . . . . . . 8 ((c_|_ ^ (c v (a ^ b))) v (c_|_ ^ (a ^ b))) = (c_|_ ^ (c v (a ^ b)))
36	35	ax-r5 37	. . . . . . 7 (((c_|_ ^ (c v (a ^ b))) v (c_|_ ^ (a ^ b))) v (c ^ (c_|_ v (a ^ b)))) = ((c_|_ ^ (c v (a ^ b))) v (c ^ (c_|_ v (a ^ b))))
37		coman1 177	. . . . . . . . . 10 (c_|_ ^ (c v (a ^ b))) C c_|_
38	37	comcom7 442	. . . . . . . . 9 (c_|_ ^ (c v (a ^ b))) C c
39		comor1 443	. . . . . . . . . . 11 (c_|_ v (a ^ b)) C c_|_
40	39	comcom7 442	. . . . . . . . . . . 12 (c_|_ v (a ^ b)) C c
41		comor2 444	. . . . . . . . . . . 12 (c_|_ v (a ^ b)) C (a ^ b)
42	40, 41	com2or 465	. . . . . . . . . . 11 (c_|_ v (a ^ b)) C (c v (a ^ b))
43	39, 42	com2an 466	. . . . . . . . . 10 (c_|_ v (a ^ b)) C (c_|_ ^ (c v (a ^ b)))
44	43	comcom 435	. . . . . . . . 9 (c_|_ ^ (c v (a ^ b))) C (c_|_ v (a ^ b))
45	38, 44	fh3 453	. . . . . . . 8 ((c_|_ ^ (c v (a ^ b))) v (c ^ (c_|_ v (a ^ b)))) = (((c_|_ ^ (c v (a ^ b))) v c) ^ ((c_|_ ^ (c v (a ^ b))) v (c_|_ v (a ^ b))))
46		ax-a2 30	. . . . . . . . . 10 ((c_|_ ^ (c v (a ^ b))) v c) = (c v (c_|_ ^ (c v (a ^ b))))
47		oml 427	. . . . . . . . . 10 (c v (c_|_ ^ (c v (a ^ b)))) = (c v (a ^ b))
48	46, 47	ax-r2 35	. . . . . . . . 9 ((c_|_ ^ (c v (a ^ b))) v c) = (c v (a ^ b))
49		or12 73	. . . . . . . . . 10 ((c_|_ ^ (c v (a ^ b))) v (c_|_ v (a ^ b))) = (c_|_ v ((c_|_ ^ (c v (a ^ b))) v (a ^ b)))
50		ax-a3 31	. . . . . . . . . . . 12 ((c_|_ v (c_|_ ^ (c v (a ^ b)))) v (a ^ b)) = (c_|_ v ((c_|_ ^ (c v (a ^ b))) v (a ^ b)))
51	50	ax-r1 34	. . . . . . . . . . 11 (c_|_ v ((c_|_ ^ (c v (a ^ b))) v (a ^ b))) = ((c_|_ v (c_|_ ^ (c v (a ^ b))