Theorem ska2 414

Description: Soundness theorem for Kalmbach's quantum propositional logic axiom KA2.

Assertion

Ref	Expression
ska2	((a == b)_|_ v ((b == c)_|_ v (a == c))) = 1

Proof of Theorem ska2

Step	Hyp	Ref	Expression
1		dfnb 87	. . 3 (a == b)_|_ = ((a v b) ^ (a_|_ v b_|_))
2		dfnb 87	. . . 4 (b == c)_|_ = ((b v c) ^ (b_|_ v c_|_))
3		dfb 86	. . . 4 (a == c) = ((a ^ c) v (a_|_ ^ c_|_))
4	2, 3	2or 67	. . 3 ((b == c)_|_ v (a == c)) = (((b v c) ^ (b_|_ v c_|_)) v ((a ^ c) v (a_|_ ^ c_|_)))
5	1, 4	2or 67	. 2 ((a == b)_|_ v ((b == c)_|_ v (a == c))) = (((a v b) ^ (a_|_ v b_|_)) v (((b v c) ^ (b_|_ v c_|_)) v ((a ^ c) v (a_|_ ^ c_|_))))
6		ax-a3 31	. . . 4 ((((a v b) ^ (a_|_ v b_|_)) v ((b v c) ^ (b_|_ v c_|_))) v ((a ^ c) v (a_|_ ^ c_|_))) = (((a v b) ^ (a_|_ v b_|_)) v (((b v c) ^ (b_|_ v c_|_)) v ((a ^ c) v (a_|_ ^ c_|_))))
7	6	ax-r1 34	. . 3 (((a v b) ^ (a_|_ v b_|_)) v (((b v c) ^ (b_|_ v c_|_)) v ((a ^ c) v (a_|_ ^ c_|_)))) = ((((a v b) ^ (a_|_ v b_|_)) v ((b v c) ^ (b_|_ v c_|_))) v ((a ^ c) v (a_|_ ^ c_|_)))
8		id 58	. . . 4 ((((a v b) ^ (a_|_ v b_|_)) v ((b v c) ^ (b_|_ v c_|_))) v ((a ^ c) v (a_|_ ^ c_|_))) = ((((a v b) ^ (a_|_ v b_|_)) v ((b v c) ^ (b_|_ v c_|_))) v ((a ^ c) v (a_|_ ^ c_|_)))
9		le1 138	. . . . 5 ((((a v b) ^ (a_|_ v b_|_)) v ((b v c) ^ (b_|_ v c_|_))) v ((a ^ c) v (a_|_ ^ c_|_))) =< 1
10		ax-a2 30	. . . . . . . . . 10 ((((a v b) ^ a_|_) v ((b_|_ ^ ((a v b) v (b v c))) v ((b v c) ^ c_|_))) v ((a ^ c) v (a_|_ ^ c_|_))) = (((a ^ c) v (a_|_ ^ c_|_)) v (((a v b) ^ a_|_) v ((b_|_ ^ ((a v b) v (b v c))) v ((b v c) ^ c_|_))))
11		or12 73	. . . . . . . . . . 11 (((a ^ c) v (a_|_ ^ c_|_)) v (((a v b) ^ a_|_) v ((b_|_ ^ ((a v b) v (b v c))) v ((b v c) ^ c_|_)))) = (((a v b) ^ a_|_) v (((a ^ c) v (a_|_ ^ c_|_)) v ((b_|_ ^ ((a v b) v (b v c))) v ((b v c) ^ c_|_))))
12		or12 73	. . . . . . . . . . . . 13 (((a v b) ^ a_|_) v ((a ^ c) v (((a_|_ ^ c_|_) v b_|_) v ((b v c) ^ c_|_)))) = ((a ^ c) v (((a v b) ^ a_|_) v (((a_|_ ^ c_|_) v b_|_) v ((b v c) ^ c_|_))))
13		or12 73	. . . . . . . . . . . . . . . 16 (((a v b) ^ a_|_) v (((a_|_ ^ c_|_) v b_|_) v ((b v c) ^ c_|_))) = (((a_|_ ^ c_|_) v b_|_) v (((a v b) ^ a_|_) v ((b v c) ^ c_|_)))
14		ax-a3 31	. . . . . . . . . . . . . . . . 17 (((a_|_ ^ c_|_) v b_|_) v (((a v b) ^ a_|_) v ((b v c) ^ c_|_))) = ((a_|_ ^ c_|_) v (b_|_ v (((a v b) ^ a_|_) v ((b v c) ^ c_|_))))
15		orordi 104	. . . . . . . . . . . . . . . . . 18 (b_|_ v (((a v b) ^ a_|_) v ((b v c) ^ c_|_))) = ((b_|_ v ((a v b) ^ a_|_)) v (b_|_ v ((b v c) ^ c_|_)))
16	15	lor 66	. . . . . . . . . . . . . . . . 17 ((a_|_ ^ c_|_) v (b_|_ v (((a v b) ^ a_|_) v ((b v c) ^ c_|_)))) = ((a_|_ ^ c_|_) v ((b_|_ v ((a v b) ^ a_|_)) v (b_|_ v ((b v c) ^ c_|_))))
17	14, 16	ax-r2 35	. . . . . . . . . . . . . . . 16 (((a_|_ ^ c_|_) v b_|_) v (((a v b) ^ a_|_) v ((b v c) ^ c_|_))) = ((a_|_ ^ c_|_) v ((b_|_ v ((a v b) ^ a_|_)) v (b_|_ v ((b v c) ^ c_|_))))
18	13, 17	ax-r2 35	. . . . . . . . . . . . . . 15 (((a v b) ^ a_|_) v (((a_|_ ^ c_|_) v b_|_) v ((b v c) ^ c_|_))) = ((a_|_ ^ c_|_) v ((b_|_ v ((a v b) ^ a_|_)) v (b_|_ v ((b v c) ^ c_|_))))
19	18	lor 66	. . . . . . . . . . . . . 14 ((a ^ c) v (((a v b) ^ a_|_) v (((a_|_ ^ c_|_) v b_|_) v ((b v c) ^ c_|_)))) = ((a ^ c) v ((a_|_ ^ c_|_) v ((b_|_ v ((a v b) ^ a_|_)) v (b_|_ v ((b v c) ^ c_|_)))))
20		or12 73	. . . . . . . . . . . . . . . 16 ((a ^ c) v ((a_|_ ^ c_|_) v ((b_|_ v a_|_) v (b_|_ v c_|_)))) = ((a_|_ ^ c_|_) v ((a ^ c) v ((b_|_ v a_|_) v (b_|_ v c_|_))))
21		le1 138	. . . . . . . . . . . . . . . . 17 ((a_|_ ^ c_|_) v ((a ^ c) v ((b_|_ v a_|_) v (b_|_ v c_|_)))) =< 1
22		df-t 40	. . . . . . . . . . . . . . . . . . . 20 1 = ((a ^ c) v (a ^ c)_|_)
23		oran3 85	. . . . . . . . . . . . . . . . . . . . . 22 (a_|_ v c_|_) = (a ^ c)_|_
24	23	lor 66	. . . . . . . . . . . . . . . . . . . . 21 ((a ^ c) v (a_|_ v c_|_)) = ((a ^ c) v (a ^ c)_|_)
25	24	ax-r1 34	. . . . . . . . . . . . . . . . . . . 20 ((a ^ c) v (a ^ c)_|_) = ((a ^ c) v (a_|_ v c_|_))
26	22, 25	ax-r2 35	. . . . . . . . . . . . . . . . . . 19 1 = ((a ^ c) v (a_|_ v c_|_))
27		leor 151	. . . . . . . . . . . . . . . . . . . . 21 a_|_ =< (b_|_ v a_|_)
28		leor 151	. . . . . . . . . . . . . . . . . . . . 21 c_|_ =< (b_|_ v c_|_)
29	27, 28	le2or 160	. . . . . . . . . . . . . . . . . . . 20 (a_|_ v c_|_) =< ((b_|_ v a_|_) v (b_|_ v c_|_))
30	29	lelor 158	. . . . . . . . . . . . . . . . . . 19 ((a ^ c) v (a_|_ v c_|_)) =< ((a ^ c) v ((b_|_ v a_|_) v (b_|_ v c_|_)))
31	26, 30	bltr 130	. . . . . . . . . . . . . . . . . 18 1 =< ((a ^ c) v ((b_|_ v a_|_) v (b_|_ v c_|_)))
32		leor 151	. . . . . . . . . . . . . . . . . 18 ((a ^ c) v ((b_|_ v a_|_) v (b_|_ v c_|_))) =< ((a_|_ ^ c_|_) v ((a ^ c) v ((b_|_ v a_|_) v (b_|_ v c_|_))))
33	31, 32	letr 129	. . . . . . . . . . . . . . . . 17 1 =< ((a_|_ ^ c_|_) v ((a ^ c) v ((b_|_ v a_|_) v (b_|_ v c_|_))))
34	21, 33	lebi 137	. . . . . . . . . . . . . . . 16 ((a_|_ ^ c_|_) v ((a ^ c) v ((b_|_ v a_|_) v (b_|_ v c_|_)))) = 1
35	20, 34	ax-r2 35	. . . . . . . . . . . . . . 15 ((a ^ c) v ((a_|_ ^ c_|_) v ((b_|_ v a_|_) v (b_|_ v c_|_)))) = 1
36		wcomorr 394	. . . . . . . . . . . . . . . . . . . . . . 23 C (b, (b v a)) = 1
37		ax-a2 30	. . . . . . . . . . . . . . . . . . . . . . . 24 (b v a) = (a v b)
38	37	bi1 110	. . . . . . . . . . . . . . . . . . . . . . 23 ((b v a) == (a v b)) = 1
39	36, 38	wcbtr 393	. . . . . . . . . . . . . . . . . . . . . 22 C (b, (a v b)) = 1
40	39	wcomcom 396	. . . . . . . . . . . . . . . . . . . . 21 C ((a v b), b) = 1
41	40	wcomcom2 397	. . . . . . . . . . . . . . . . . . . 20 C ((a v b), b_|_) = 1
42		wcomorr 394	. . . . . . . . . . . . . . . . . . . . . 22 C (a, (a v b)) = 1
43	42	wcomcom 396	. . . . . . . . . . . . . . . . . . . . 21 C ((a v b), a) = 1
44	43	wcomcom2 397	. . . . . . . . . . . . . . . . . . . 20 C ((a v b), a_|_) = 1
45	41, 44	wfh4 408	. . . . . . . . . . . . . . . . . . 19 ((b_|_ v ((a v b) ^ a_|_)) == ((b_|_ v (a v b)) ^ (b_|_ v a_|_))) = 1
46		or12 73	. . . . . . . . . . . . . . . . . . . . . . 23 (b_|_ v (a