QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ska2 Unicode version
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
StepHypRef 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'))
42, 32or 72 . . 3 ((b == c)' v (a == c)) = (((b v c) ^ (b' v c')) v ((a ^ c) v (a' ^ c')))
51, 42or 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'))))
76ax-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')))
1615lor 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'))))
1714, 16ax-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'))))
1813, 17ax-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'))))
1918lor 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)'
2423lor 70 . . . . . . . . . . . . . . . . . . . . 21 ((a ^ c) v (a' v c')) = ((a ^ c) v (a ^ c)')
2524ax-r1 35 . . . . . . . . . . . . . . . . . . . 20 ((a ^ c) v (a ^ c)') = ((a ^ c) v (a' v c'))
2622, 25ax-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')
2927, 28le2or 168 . . . . . . . . . . . . . . . . . . . 20 (a' v c') =< ((b' v a') v (b' v c'))
3029lelor 166 . . . . . . . . . . . . . . . . . . 19 ((a ^ c) v (a' v c')) =< ((a ^ c) v ((b' v a') v (b' v c')))
3126, 30bltr 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'))))
3331, 32letr 137 . . . . . . . . . . . . . . . . 17 1 =< ((a' ^ c') v ((a ^ c) v ((b' v a') v (b' v c'))))
3421, 33lebi 145 . . . . . . . . . . . . . . . 16 ((a' ^ c') v ((a ^ c) v ((b' v a') v (b' v c')))) = 1
3520, 34ax-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)
3837bi1 118 . . . . . . . . . . . . . . . . . . . . . . 23 ((b v a) == (a v b)) = 1
3936, 38wcbtr 411 . . . . . . . . . . . . . . . . . . . . . 22 C (b, (a v b)) = 1
4039wcomcom 414 . . . . . . . . . . . . . . . . . . . . 21 C ((a v b), b) = 1
4140wcomcom2 415 . . . . . . . . . . . . . . . . . . . 20 C ((a v b), b') = 1
42 wcomorr 412 . . . . . . . . . . . . . . . . . . . . . 22 C (a, (a v b)) = 1
4342wcomcom 414 . . . . . . . . . . . . . . . . . . . . 21 C ((a v b), a) = 1
4443wcomcom2 415 . . . . . . . . . . . . . . . . . . . 20 C ((a v b), a') = 1
4541, 44wfh4 426 . . . . . . . . . . . . . . . . . . 19 ((b' v ((a v b) ^ a')) == ((b' v (a v b)) ^ (b' v a'))) = 1
46 or12 80 . . . . . . . . . . . . . . . . . . . . . . 23 (b' v (a v b)) = (a v (b' v b))
47 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b' v b) = (b v b')
48 df-t 41 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 = (b v b')
4948ax-r1 35 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b v b') = 1
5047, 49ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . . . 25 (b' v b) = 1
5150lor 70 . . . . . . . . . . . . . . . . . . . . . . . 24 (a v (b' v b)) = (a v 1)
52 or1 104 . . . . . . . . . . . . . . . . . . . . . . . 24 (a v 1) = 1
5351, 52ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . 23 (a v (b' v b)) = 1
5446, 53ax-r2 36 . . . . . . . . . . . . . . . . . . . . . 22 (b' v (a v b)) = 1
5554ran 78 . . . . . . . . . . . . . . . . . . . . 21 ((b' v (a v b)) ^ (b' v a')) = (1 ^ (b' v a'))
56 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 (1 ^ (b' v a')) = ((b' v a') ^ 1)
57 an1 106 . . . . . . . . . . . . . . . . . . . . . 22 ((b' v a') ^ 1) = (b' v a')
5856, 57ax-r2 36 . . . . . . . . . . . . . . . . . . . . 21 (1 ^ (b' v a')) = (b' v a')
5955, 58ax-r2 36 . . . . . . . . . . . . . . . . . . . 20 ((b' v (a v b)) ^ (b' v a')) = (b' v a')
6059bi1 118 . . . . . . . . . . . . . . . . . . 19 (((b' v (a v b)) ^ (b' v a')) == (b' v a')) = 1
6145, 60wr2 371 . . . . . . . . . . . . . . . . . 18 ((b' v ((a v b) ^ a')) == (b' v a')) = 1
62 wcomorr 412 . . . . . . . . . . . . . . . . . . . . . 22 C (b, (b v c)) = 1
6362wcomcom 414 . . . . . . . . . . . . . . . . . . . . 21 C ((b v c), b) = 1
6463wcomcom2 415 . . . . . . . . . . . . . . . . . . . 20 C ((b v c), b') = 1
65 wcomorr 412 . . . . . . . . . . . . . . . . . . . . . . 23 C (c, (c v b)) = 1
66 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . 24 (c v b) = (b v c)
6766bi1 118 . . . . . . . . . . . . . . . . . . . . . . 23 ((c v b) == (b v c)) = 1
6865, 67wcbtr 411 . . . . . . . . . . . . . . . . . . . . . 22 C (c, (b v c)) = 1
6968wcomcom 414 . . . . . . . . . . . . . . . . . . . . 21 C ((b v c), c) = 1
7069wcomcom2 415 . . . . . . . . . . . . . . . . . . . 20 C ((b v c), c') = 1
7164, 70wfh4 426 . . . . . . . . . . . . . . . . . . 19 ((b' v ((b v c) ^ c')) == ((b' v (b v c)) ^ (b' v c'))) = 1
72 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . 23 (b' v (b v c)) = ((b v c) v b')
73 or32 82 . . . . . . . . . . . . . . . . . . . . . . . 24 ((b v c) v b') = ((b v b') v c)
74 ax-a2 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((b v b') v c) = (c v (b v b'))
7549lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (c v (b v b')) = (c v 1)
76 or1 104 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (c v 1) = 1
7775, 76ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . . . 25 (c v (b v b')) = 1
7874, 77ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . . 24 ((b v b') v c) = 1
7973, 78ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . 23 ((b v c) v b') = 1
8072, 79ax-r2 36 . . . . . . . . . . . . . . . . . . . . . 22 (b' v (b v c)) = 1
8180ran 78 . . . . . . . . . . . . . . . . . . . . 21 ((b' v (b v c)) ^ (b' v c')) = (1 ^ (b' v c'))
82 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 (1 ^ (b' v c')) = ((b' v c') ^ 1)
83 an1 106 . . . . . . . . . . . . . . . . . . . . . 22 ((b' v c') ^ 1) = (b' v c')
8482, 83ax-r2 36 . . . . . . . . . . . . . . . . . . . . 21 (1 ^ (b' v c')) = (b' v c')
8581, 84ax-r2 36 . . . . . . . . . . . . . . . . . . . 20 ((b' v (b v c)) ^ (b' v c')) = (b' v c')
8685bi1 118 . . . . . . . . . . . . . . . . . . 19 (((b' v (b v c)) ^ (b' v c')) == (b' v c')) = 1
8771, 86wr2 371 . . . . . . . . . . . . . . . . . 18 ((b' v ((b v c) ^ c')) == (b' v c')) = 1
8861, 87w2or 372 . . . . . . . . . . . . . . . . 17 (((b' v ((a v b) ^ a')) v (b' v ((b v c) ^ c'))) == ((b' v a') v (b' v c'))) = 1
8988wlor 368 . . . . . . . . . . . . . . . 16 (((a' ^ c') v ((b' v ((a v b) ^ a')) v (b' v ((b v c) ^ c')))) == ((a' ^ c') v ((b' v a') v (b' v c')))) = 1
9089wlor 368 . . . . . . . . . . . . . . 15 (((a ^ c) v ((a' ^ c') v ((b' v ((a v b) ^ a')) v (b' v ((b v c) ^ c'))))) == ((a ^ c) v ((a' ^ c') v ((b' v a') v (b' v c'))))) = 1
9135, 90wwbmpr 206 . . . . . . . . . . . . . 14 ((a ^ c) v ((a' ^ c') v ((b' v ((a v b) ^ a')) v (b' v ((b v c) ^ c'))))) = 1
9219, 91ax-r2 36 . . . . . . . . . . . . 13 ((a ^ c) v (((a v b) ^ a') v (((a' ^ c') v b') v ((b v c) ^ c')))) = 1
9312, 92ax-r2 36 . . . . . . . . . . . 12 (((a v b) ^ a') v ((a ^ c) v (((a' ^ c') v b') v ((b v c) ^ c')))) = 1
94 ax-a3 32 . . . . . . . . . . . . . . 15 (((a ^ c) v (a' ^ c')) v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c'))) = ((a ^ c) v ((a' ^ c') v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c'))))
9594bi1 118 . . . . . . . . . . . . . 14 ((((a ^ c) v (a' ^ c')) v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c'))) == ((a ^ c) v ((a' ^ c') v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c'))))) = 1
96 ax-a3 32 . . . . . . . . . . . . . . . . . 18 (((a' ^ c') v (b' ^ ((a v b) v (b v c)))) v ((b v c) ^ c')) = ((a' ^ c') v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c')))
9796ax-r1 35 . . . . . . . . . . . . . . . . 17 ((a' ^ c') v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c'))) = (((a' ^ c') v (b' ^ ((a v b) v (b v c)))) v ((b v c) ^ c'))
9897bi1 118 . . . . . . . . . . . . . . . 16 (((a' ^ c') v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c'))) == (((a' ^ c') v (b' ^ ((a v b) v (b v c)))) v ((b v c) ^ c'))) = 1
99 ancom 74 . . . . . . . . . . . . . . . . . . . 20 (b' ^ ((a v b) v (b v c))) = (((a v b) v (b v c)) ^ b')
10099lor 70 . . . . . . . . . . . . . . . . . . 19 ((a' ^ c') v (b' ^ ((a v b) v (b v c)))) = ((a' ^ c') v (((a v b) v (b v c)) ^ b'))
101100bi1 118 . . . . . . . . . . . . . . . . . 18 (((a' ^ c') v (b' ^ ((a v b) v (b v c)))) == ((a' ^ c') v (((a v b) v (b v c)) ^ b'))) = 1
102 wcomorr 412 . . . . . . . . . . . . . . . . . . . . . . . 24 C ((a v c), ((a v c) v b)) = 1
103 orordir 113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a v c) v b) = ((a v b) v (c v b))
10466lor 70 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a v b) v (c v b)) = ((a v b) v (b v c))
105103, 104ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a v c) v b) = ((a v b) v (b v c))
106105bi1 118 . . . . . . . . . . . . . . . . . . . . . . . 24 (((a v c) v b) == ((a v b) v (b v c))) = 1
107102, 106wcbtr 411 . . . . . . . . . . . . . . . . . . . . . . 23 C ((a v c), ((a v b) v (b v c))) = 1
108107wcomcom 414 . . . . . . . . . . . . . . . . . . . . . 22 C (((a v b) v (b v c)), (a v c)) = 1
109108wcomcom2 415 . . . . . . . . . . . . . . . . . . . . 21 C (((a v b) v (b v c)), (a v c)') = 1
110 anor3 90 . . . . . . . . . . . . . . . . . . . . . . 23 (a' ^ c') = (a v c)'
111110ax-r1 35 . . . . . . . . . . . . . . . . . . . . . 22 (a v c)' = (a' ^ c')
112111bi1 118 . . . . . . . . . . . . . . . . . . . . 21 ((a v c)' == (a' ^ c')) = 1
113109, 112wcbtr 411 . . . . . . . . . . . . . . . . . . . 20 C (((a v b) v (b v c)), (a' ^ c')) = 1
11439, 62wcom2or 427 . . . . . . . . . . . . . . . . . . . . . 22 C (b, ((a v b) v (b v c))) = 1
115114wcomcom 414 . . . . . . . . . . . . . . . . . . . . 21 C (((a v b) v (b v c)), b) = 1
116115wcomcom2 415 . . . . . . . . . . . . . . . . . . . 20 C (((a v b) v (b v c)), b') = 1
117113, 116wfh4 426 . . . . . . . . . . . . . . . . . . 19 (((a' ^ c') v (((a v b) v (b v c)) ^ b')) == (((a' ^ c') v ((a v b) v (b v c))) ^ ((a' ^ c') v b'))) = 1
118 le1 146 . . . . . . . . . . . . . . . . . . . . . . 23 ((a' ^ c') v ((a v b) v (b v c))) =< 1
119 df-t 41 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 = ((a' ^ c') v (a' ^ c')')
120 oran 87 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a v c) = (a' ^ c')'
121120ax-r1 35 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a' ^ c')' = (a v c)
122121lor 70 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a' ^ c') v (a' ^ c')') = ((a' ^ c') v (a v c))
123119, 122ax-r2 36 . . . . . . . . . . . . . . . . . . . . . . . 24 1 = ((a' ^ c') v (a v c))
124 leo 158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 a =< (a v b)
125 leor 159 . . . . . . . . . . . . . . . . . . . . . . . . . 26 c =< (b v c)
126124, 125le2or 168 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a v c) =< ((a v b) v (b v c))
127126lelor 166 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a' ^ c') v (a v c)) =< ((a' ^ c') v ((a v b) v (b v c)))
128123, 127bltr 138 . . . . . . . . . . . . . . . . . . . . . . 23 1 =< ((a' ^ c') v ((a v b) v (b v c)))
129118, 128lebi 145 . . . . . . . . . . . . . . . . . . . . . 22 ((a' ^ c') v ((a v b) v (b v c))) = 1
130129ran 78 . . . . . . . . . . . . . . . . . . . . 21 (((a' ^ c') v ((a v b) v (b v c))) ^ ((a' ^ c') v b')) = (1 ^ ((a' ^ c') v b'))
131 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 (1 ^ ((a' ^ c') v b')) = (((a' ^ c') v b') ^ 1)
132 an1 106 . . . . . . . . . . . . . . . . . . . . . 22 (((a' ^ c') v b') ^ 1) = ((a' ^ c') v b')
133131, 132ax-r2 36 . . . . . . . . . . . . . . . . . . . . 21 (1 ^ ((a' ^ c') v b')) = ((a' ^ c') v b')
134130, 133ax-r2 36 . . . . . . . . . . . . . . . . . . . 20 (((a' ^ c') v ((a v b) v (b v c))) ^ ((a' ^ c') v b')) = ((a' ^ c') v b')
135134bi1 118 . . . . . . . . . . . . . . . . . . 19 ((((a' ^ c') v ((a v b) v (b v c))) ^ ((a' ^ c') v b')) == ((a' ^ c') v b')) = 1
136117, 135wr2 371 . . . . . . . . . . . . . . . . . 18 (((a' ^ c') v (((a v b) v (b v c)) ^ b')) == ((a' ^ c') v b')) = 1
137101, 136wr2 371 . . . . . . . . . . . . . . . . 17 (((a' ^ c') v (b' ^ ((a v b) v (b v c)))) == ((a' ^ c') v b')) = 1
138137wr5-2v 366 . . . . . . . . . . . . . . . 16 ((((a' ^ c') v (b' ^ ((a v b) v (b v c)))) v ((b v c) ^ c')) == (((a' ^ c') v b') v ((b v c) ^ c'))) = 1
13998, 138wr2 371 . . . . . . . . . . . . . . 15 (((a' ^ c') v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c'))) == (((a' ^ c') v b') v ((b v c) ^ c'))) = 1
140139wlor 368 . . . . . . . . . . . . . 14 (((a ^ c) v ((a' ^ c') v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c')))) == ((a ^ c) v (((a' ^ c') v b') v ((b v c) ^ c')))) = 1
14195, 140wr2 371 . . . . . . . . . . . . 13 ((((a ^ c) v (a' ^ c')) v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c'))) == ((a ^ c) v (((a' ^ c') v b') v ((b v c) ^ c')))) = 1
142141wlor 368 . . . . . . . . . . . 12 ((((a v b) ^ a') v (((a ^ c) v (a' ^ c')) 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') v ((b v c) ^ c'))))) = 1
14393, 142wwbmpr 206 . . . . . . . . . . 11 (((a v b) ^ a') v (((a ^ c) v (a' ^ c')) v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c')))) = 1
14411, 143ax-r2 36 . . . . . . . . . 10 (((a ^ c) v (a' ^ c')) v (((a v b) ^ a') v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c')))) = 1
14510, 144ax-r2 36 . . . . . . . . 9 ((((a v b) ^ a') v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c'))) v ((a ^ c) v (a' ^ c'))) = 1
14639wcomcom3 416 . . . . . . . . . . . . 13 C (b', (a v b)) = 1
14762wcomcom3 416 . . . . . . . . . . . . 13 C (b', (b v c)) = 1
148146, 147wfh1 423 . . . . . . . . . . . 12 ((b' ^ ((a v b) v (b v c))) == ((b' ^ (a v b)) v (b' ^ (b v c)))) = 1
149148wr5-2v 366 . . . . . . . . . . 11 (((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c')) == (((b' ^ (a v b)) v (b' ^ (b v c))) v ((b v c) ^ c'))) = 1
150149wlor 368 . . . . . . . . . 10 ((((a v b) ^ a') v ((b' ^ ((a v b) v (b v c))) v ((b v c) ^ c'))) == (((a v b) ^ a') v (((b' ^ (a v b)) v (b' ^ (b v c))) v ((b v c) ^ c')))) = 1
151150wr5-2v 366 . . . . . . . . 9 (((((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 v b) ^ a') v (((b' ^ (a v b)) v (b' ^ (b v c))) v ((b v c) ^ c'))) v ((a ^ c) v (a' ^ c')))) = 1
152145, 151wwbmp 205 . . . . . . . 8 ((((a v b) ^ a') v (((b' ^ (a v b)) v (b' ^ (b v c))) v ((b v c) ^ c'))) v ((a ^ c) v (a' ^ c'))) = 1
153152ax-r1 35 . . . . . . 7 1 = ((((a v b) ^ a') v (((b' ^ (a v b)) v (b' ^ (b v c))) v ((b v c) ^ c'))) v ((a ^ c) v (a' ^ c')))
154 ax-a3 32 . . . . . . . . . . 11 ((((a v b) ^ a') v ((b' ^ (a v b)) v (b' ^ (b v c)))) v ((b v c) ^ c')) = (((a v b) ^ a') v (((b' ^ (a v b)) v (b' ^ (b v c))) v ((b v c) ^ c')))
155154ax-r1 35 . . . . . . . . . 10 (((a v b) ^ a') v (((b' ^ (a v b)) v (b' ^ (b v c))) v ((b v c) ^ c'))) = ((((a v b) ^ a') v ((b' ^ (a v b)) v (b' ^ (b v c)))) v ((b v c) ^ c'))
156 ax-a3 32 . . . . . . . . . . . 12 ((((a v b) ^ a') v (b' ^ (a v b))) v (b' ^ (b v c))) = (((a v b) ^ a') v ((b' ^ (a v b)) v (b' ^ (b v c))))
157156ax-r1 35 . . . . . . . . . . 11 (((a v b) ^ a') v ((b' ^ (a v b)) v (b' ^ (b v c)))) = ((((a v b) ^ a') v (b' ^ (a v b))) v (b' ^ (b v c)))
158157ax-r5 38 . . . . . . . . . 10 ((((a v b) ^ a') v ((b' ^ (a v b)) v (b' ^ (b v c)))) v ((b v c) ^ c')) = (((((a v b) ^ a') v (b' ^ (a v b))) v (b' ^ (b v c))) v ((b v c) ^ c'))
159155, 158ax-r2 36 . . . . . . . . 9 (((a v b) ^ a') v (((b' ^ (a v b)) v (b' ^ (b v c))) v ((b v c) ^ c'))) = (((((a v b) ^ a') v (b' ^ (a v b))) v (b' ^ (b v c))) v ((b v c) ^ c'))
160 ax-a3 32 . . . . . . . . 9 (((((a v b) ^ a') v (b' ^ (a v b))) v (b' ^ (b v c))) v ((b v c) ^ c')) = ((((a v b) ^ a') v (b' ^ (a v b))) v ((b' ^ (b v c)) v ((b v c) ^ c')))
161159, 160ax-r2 36 . . . . . . . 8 (((a v b) ^ a') v (((b' ^ (a v b)) v (b' ^ (b v c))) v ((b v c) ^ c'))) = ((((a v b) ^ a') v (b' ^ (a v b))) v ((b' ^ (b v c)) v ((b v c) ^ c')))
162161ax-r5 38 . . . . . . 7 ((((a v b) ^ a') v (((b' ^ (a v b)) v (b' ^ (b v c))) v ((b v c) ^ c'))) v ((a ^ c) v (a' ^ c'))) = (((((a v b) ^ a') v (b' ^ (a v b))) v ((b' ^ (b v c)) v ((b v c) ^ c'))) v ((a ^ c) v (a' ^ c')))
163153, 162ax-r2 36 . . . . . 6 1 = (((((a v b) ^ a') v (b' ^ (a v b))) v ((b' ^ (b v c)) v ((b v c) ^ c'))) v ((a ^ c) v (a' ^ c')))
164 ancom 74 . . . . . . . . . 10 (b' ^ (a v b)) = ((a v b) ^ b')
165164lor 70 . . . . . . . . 9 (((a v b) ^ a') v (b' ^ (a v b))) = (((a v b) ^ a') v ((a v b) ^ b'))
166 ledi 174 . . . . . . . . 9 (((a v b) ^ a') v ((a v b) ^ b')) =< ((a v b) ^ (a' v b'))
167165, 166bltr 138 . . . . . . . 8 (((a v b) ^ a') v (b' ^ (a v b))) =< ((a v b) ^ (a' v b'))
168 ancom 74 . . . . . . . . . 10 (b' ^ (b v c)) = ((b v c) ^ b')
169168ax-r5 38 . . . . . . . . 9 ((b' ^ (b v c)) v ((b v c) ^ c')) = (((b v c) ^ b') v ((b v c) ^ c'))
170 ledi 174 . . . . . . . . 9 (((b v c) ^ b') v ((b v c) ^ c')) =< ((b v c) ^ (b' v c'))
171169, 170bltr 138 . . . . . . . 8 ((b' ^ (b v c)) v ((b v c) ^ c')) =< ((b v c) ^ (b' v c'))
172167, 171le2or 168 . . . . . . 7 ((((a v b) ^ a') v (b' ^ (a v b))) v ((b' ^ (b v c)) v ((b v c) ^ c'))) =< (((a v b) ^ (a' v b')) v ((b v c) ^ (b' v c')))
173172leror 152 . . . . . 6 (((((a v b) ^ a') v (b' ^ (a v b))) v ((b' ^ (b v c)) v ((b v c) ^ 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')))
174163, 173bltr 138 . . . . 5 1 =< ((((a v b) ^ (a' v b')) v ((b v c) ^ (b' v c'))) v ((a ^ c) v (a' ^ c')))
1759, 174lebi 145 . . . 4 ((((a v b) ^ (a' v b')) v ((b v c) ^ (b' v c'))) v ((a ^ c) v (a' ^ c'))) = 1
1768, 175ax-r2 36 . . 3 ((((a v b) ^ (a' v b')) v ((b v c) ^ (b' v c'))) v ((a ^ c) v (a' ^ c'))) = 1
1777, 176ax-r2 36 . 2 (((a v b) ^ (a' v b')) v (((b v c) ^ (b' v c')) v ((a ^ c) v (a' ^ c')))) = 1
1785, 177ax-r2 36 1 ((a == b)' v ((b == c)' v (a == c))) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-wom 361
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134
This theorem is referenced by:  u3lemax5  797
  Copyright terms: Public domain W3C validator