Theorem ska2 432

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 95	. . 3 (a == b)' = ((a v b) ^ (a' v b'))
2		dfnb 95	. . . 4 (b == c)' = ((b v c) ^ (b' v c'))
3		dfb 94	. . . 4 (a == c) = ((a ^ c) v (a' ^ c'))
4	2, 3	2or 72	. . 3 ((b == c)' v (a == c)) = (((b v c) ^ (b' v c')) v ((a ^ c) v (a' ^ c')))
5	1, 4	2or 72	. 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 32	. . . 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 35	. . 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 59	. . . 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 146	. . . . 5 ((((a v b) ^ (a' v b')) v ((b v c) ^ (b' v c'))) v ((a ^ c) v (a' ^ c'))) =< 1
10		ax-a2 31	. . . . . . . . . 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 80	. . . . . . . . . . 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 80	. . . . . . . . . . . . 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 80	. . . . . . . . . . . . . . . 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 32	. . . . . . . . . . . . . . . . 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 112	. . . . . . . . . . . . . . . . . 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 70	. . . . . . . . . . . . . . . . 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 36	. . . . . . . . . . . . . . . 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 36	. . . . . . . . . . . . . . 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 70	. . . . . . . . . . . . . 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 80	. . . . . . . . . . . . . . . 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 146	. . . . . . . . . . . . . . . . 17 ((a' ^ c') v ((a ^ c) v ((b' v a') v (b' v c')))) =< 1
22		df-t 41	. . . . . . . . . . . . . . . . . . . 20 1 = ((a ^ c) v (a ^ c)')
23		oran3 93	. . . . . . . . . . . . . . . . . . . . . 22 (a' v c') = (a ^ c)'
24	23	lor 70	. . . . . . . . . . . . . . . . . . . . 21 ((a ^ c) v (a' v c')) = ((a ^ c) v (a ^ c)')
25	24	ax-r1 35	. . . . . . . . . . . . . . . . . . . 20 ((a ^ c) v (a ^ c)') = ((a ^ c) v (a' v c'))
26	22, 25	ax-r2 36	. . . . . . . . . . . . . . . . . . 19 1 = ((a ^ c) v (a' v c'))
27		leor 159	. . . . . . . . . . . . . . . . . . . . 21 a' =< (b' v a')
28		leor 159	. . . . . . . . . . . . . . . . . . . . 21 c' =< (b' v c')
29	27, 28	le2or 168	. . . . . . . . . . . . . . . . . . . 20 (a' v c') =< ((b' v a') v (b' v c'))
30	29	lelor 166	. . . . . . . . . . . . . . . . . . 19 ((a ^ c) v (a' v c')) =< ((a ^ c) v ((b' v a') v (b' v c')))
31	26, 30	bltr 138	. . . . . . . . . . . . . . . . . 18 1 =< ((a ^ c) v ((b' v a') v (b' v c')))
32		leor 159	. . . . . . . . . . . . . . . . . 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 137	. . . . . . . . . . . . . . . . 17 1 =< ((a' ^ c') v ((a ^ c) v ((b' v a') v (b' v c'))))
34	21, 33	lebi 145	. . . . . . . . . . . . . . . 16 ((a' ^ c') v ((a ^ c) v ((b' v a') v (b' v c')))) = 1
35	20, 34	ax-r2 36	. . . . . . . . . . . . . . 15 ((a ^ c) v ((a' ^ c') v ((b' v a') v (b' v c')))) = 1
36		wcomorr 412	. . . . . . . . . . . . . . . . . . . . . . 23 C (b, (b v a)) = 1
37		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . 24 (b v a) = (a v b)
38	37	bi1 118	. . . . . . . . . . . . . . . . . . . . . . 23 ((b v a) == (a v b)) = 1
39	36, 38	wcbtr 411	. . . . . . . . . . . . . . . . . . . . . 22 C (b, (a v b)) = 1
40	39	wcomcom 414	. . . . . . . . . . . . . . . . . . . . 21 C ((a v b), b) = 1
41	40	wcomcom2 415	. . . . . . . . . . . . . . . . . . . 20 C ((a v b), b') = 1
42		wcomorr 412	. . . . . . . . . . . . . . . . . . . . . 22 C (a, (a v b)) = 1
43	42	wcomcom 414	. . . . . . . . . . . . . . . . . . . . 21 C ((a v b), a) = 1
44	43	wcomcom2 415	. . . . . . . . . . . . . . . . . . . 20 C ((a v b), a') = 1
45	41, 44	wfh4 426	. . . . . . . . . . . . . . . . . . 19 ((b' v ((a v b) ^ a')) == ((b' v (a v b)) ^