QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  i3con Unicode version
Theorem i3con 551
Description: Theorem for Kalmbach implication.
Assertion
Ref Expression
i3con ((a ->3 b) ->3 ((a ->3 b) ->3 (b' ->3 a'))) = 1
Proof of Theorem i3con
StepHypRef Expression
1 ni32 502 . . . . 5 (a ->3 b)' = ((a v b) ^ ((a ^ b') v (a' ^ (a v b'))))
2 i3n1 249 . . . . 5 (b' ->3 a') = (((b ^ a') v (b ^ a)) v (b' ^ (b v a')))
31, 22or 72 . . . 4 ((a ->3 b)' v (b' ->3 a')) = (((a v b) ^ ((a ^ b') v (a' ^ (a v b')))) v (((b ^ a') v (b ^ a)) v (b' ^ (b v a'))))
4 ax-a2 31 . . . . 5 (((a v b) ^ ((a ^ b') v (a' ^ (a v b')))) v (((b ^ a') v (b ^ a)) v (b' ^ (b v a')))) = ((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v ((a v b) ^ ((a ^ b') v (a' ^ (a v b')))))
5 comor2 462 . . . . . . . . . 10 (a v b) C b
6 comor1 461 . . . . . . . . . . 11 (a v b) C a
76comcom2 183 . . . . . . . . . 10 (a v b) C a'
85, 7com2an 484 . . . . . . . . 9 (a v b) C (b ^ a')
95, 6com2an 484 . . . . . . . . 9 (a v b) C (b ^ a)
108, 9com2or 483 . . . . . . . 8 (a v b) C ((b ^ a') v (b ^ a))
115comcom2 183 . . . . . . . . 9 (a v b) C b'
125, 7com2or 483 . . . . . . . . 9 (a v b) C (b v a')
1311, 12com2an 484 . . . . . . . 8 (a v b) C (b' ^ (b v a'))
1410, 13com2or 483 . . . . . . 7 (a v b) C (((b ^ a') v (b ^ a)) v (b' ^ (b v a')))
156, 11com2an 484 . . . . . . . 8 (a v b) C (a ^ b')
166, 11com2or 483 . . . . . . . . 9 (a v b) C (a v b')
177, 16com2an 484 . . . . . . . 8 (a v b) C (a' ^ (a v b'))
1815, 17com2or 483 . . . . . . 7 (a v b) C ((a ^ b') v (a' ^ (a v b')))
1914, 18fh4 472 . . . . . 6 ((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v ((a v b) ^ ((a ^ b') v (a' ^ (a v b'))))) = (((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v (a v b)) ^ ((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v ((a ^ b') v (a' ^ (a v b')))))
20 ax-a3 32 . . . . . . . 8 ((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v (a v b)) = (((b ^ a') v (b ^ a)) v ((b' ^ (b v a')) v (a v b)))
21 or12 80 . . . . . . . . 9 (((b ^ a') v (b ^ a)) v ((b' ^ (b v a')) v (a v b))) = ((b' ^ (b v a')) v (((b ^ a') v (b ^ a)) v (a v b)))
22 ax-a3 32 . . . . . . . . . . . 12 (((b ^ a') v (b ^ a)) v (a v b)) = ((b ^ a') v ((b ^ a) v (a v b)))
23 ancom 74 . . . . . . . . . . . . . . . . 17 (b ^ a) = (a ^ b)
24 lea 160 . . . . . . . . . . . . . . . . 17 (a ^ b) =< a
2523, 24bltr 138 . . . . . . . . . . . . . . . 16 (b ^ a) =< a
26 leo 158 . . . . . . . . . . . . . . . 16 a =< (a v b)
2725, 26letr 137 . . . . . . . . . . . . . . 15 (b ^ a) =< (a v b)
2827df-le2 131 . . . . . . . . . . . . . 14 ((b ^ a) v (a v b)) = (a v b)
2928lor 70 . . . . . . . . . . . . 13 ((b ^ a') v ((b ^ a) v (a v b))) = ((b ^ a') v (a v b))
30 ax-a2 31 . . . . . . . . . . . . . 14 ((b ^ a') v (a v b)) = ((a v b) v (b ^ a'))
31 ax-a3 32 . . . . . . . . . . . . . . 15 ((a v b) v (b ^ a')) = (a v (b v (b ^ a')))
32 orabs 120 . . . . . . . . . . . . . . . 16 (b v (b ^ a')) = b
3332lor 70 . . . . . . . . . . . . . . 15 (a v (b v (b ^ a'))) = (a v b)
3431, 33ax-r2 36 . . . . . . . . . . . . . 14 ((a v b) v (b ^ a')) = (a v b)
3530, 34ax-r2 36 . . . . . . . . . . . . 13 ((b ^ a') v (a v b)) = (a v b)
3629, 35ax-r2 36 . . . . . . . . . . . 12 ((b ^ a') v ((b ^ a) v (a v b))) = (a v b)
3722, 36ax-r2 36 . . . . . . . . . . 11 (((b ^ a') v (b ^ a)) v (a v b)) = (a v b)
3837lor 70 . . . . . . . . . 10 ((b' ^ (b v a')) v (((b ^ a') v (b ^ a)) v (a v b))) = ((b' ^ (b v a')) v (a v b))
39 ax-a2 31 . . . . . . . . . . 11 ((b' ^ (b v a')) v (a v b)) = ((a v b) v (b' ^ (b v a')))
405comcom 453 . . . . . . . . . . . . . 14 b C (a v b)
4140comcom3 454 . . . . . . . . . . . . 13 b' C (a v b)
42 comorr 184 . . . . . . . . . . . . . 14 b C (b v a')
4342comcom3 454 . . . . . . . . . . . . 13 b' C (b v a')
4441, 43fh4 472 . . . . . . . . . . . 12 ((a v b) v (b' ^ (b v a'))) = (((a v b) v b') ^ ((a v b) v (b v a')))
45 ax-a3 32 . . . . . . . . . . . . . . 15 ((a v b) v b') = (a v (b v b'))
46 df-t 41 . . . . . . . . . . . . . . . . . 18 1 = (b v b')
4746ax-r1 35 . . . . . . . . . . . . . . . . 17 (b v b') = 1
4847lor 70 . . . . . . . . . . . . . . . 16 (a v (b v b')) = (a v 1)
49 or1 104 . . . . . . . . . . . . . . . 16 (a v 1) = 1
5048, 49ax-r2 36 . . . . . . . . . . . . . . 15 (a v (b v b')) = 1
5145, 50ax-r2 36 . . . . . . . . . . . . . 14 ((a v b) v b') = 1
52 ax-a2 31 . . . . . . . . . . . . . . . 16 (a v b) = (b v a)
5352ax-r5 38 . . . . . . . . . . . . . . 15 ((a v b) v (b v a')) = ((b v a) v (b v a'))
54 or4 84 . . . . . . . . . . . . . . . 16 ((b v a) v (b v a')) = ((b v b) v (a v a'))
55 df-t 41 . . . . . . . . . . . . . . . . . . 19 1 = (a v a')
5655ax-r1 35 . . . . . . . . . . . . . . . . . 18 (a v a') = 1
5756lor 70 . . . . . . . . . . . . . . . . 17 ((b v b) v (a v a')) = ((b v b) v 1)
58 or1 104 . . . . . . . . . . . . . . . . 17 ((b v b) v 1) = 1
5957, 58ax-r2 36 . . . . . . . . . . . . . . . 16 ((b v b) v (a v a')) = 1
6054, 59ax-r2 36 . . . . . . . . . . . . . . 15 ((b v a) v (b v a')) = 1
6153, 60ax-r2 36 . . . . . . . . . . . . . 14 ((a v b) v (b v a')) = 1
6251, 612an 79 . . . . . . . . . . . . 13 (((a v b) v b') ^ ((a v b) v (b v a'))) = (1 ^ 1)
63 an1 106 . . . . . . . . . . . . 13 (1 ^ 1) = 1
6462, 63ax-r2 36 . . . . . . . . . . . 12 (((a v b) v b') ^ ((a v b) v (b v a'))) = 1
6544, 64ax-r2 36 . . . . . . . . . . 11 ((a v b) v (b' ^ (b v a'))) = 1
6639, 65ax-r2 36 . . . . . . . . . 10 ((b' ^ (b v a')) v (a v b)) = 1
6738, 66ax-r2 36 . . . . . . . . 9 ((b' ^ (b v a')) v (((b ^ a') v (b ^ a)) v (a v b))) = 1
6821, 67ax-r2 36 . . . . . . . 8 (((b ^ a') v (b ^ a)) v ((b' ^ (b v a')) v (a v b))) = 1
6920, 68ax-r2 36 . . . . . . 7 ((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v (a v b)) = 1
70 ax-a3 32 . . . . . . . 8 ((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v ((a ^ b') v (a' ^ (a v b')))) = (((b ^ a') v (b ^ a)) v ((b' ^ (b v a')) v ((a ^ b') v (a' ^ (a v b')))))
71 ax-a2 31 . . . . . . . . . . 11 ((b ^ a') v (b ^ a)) = ((b ^ a) v (b ^ a'))
72 ancom 74 . . . . . . . . . . . 12 (b ^ a') = (a' ^ b)
7372lor 70 . . . . . . . . . . 11 ((b ^ a) v (b ^ a')) = ((b ^ a) v (a' ^ b))
7471, 73ax-r2 36 . . . . . . . . . 10 ((b ^ a') v (b ^ a)) = ((b ^ a) v (a' ^ b))
75 ax-a3 32 . . . . . . . . . . . 12 (((b' ^ (b v a')) v (a ^ b')) v (a' ^ (a v b'))) = ((b' ^ (b v a')) v ((a ^ b') v (a' ^ (a v b'))))
7675ax-r1 35 . . . . . . . . . . 11 ((b' ^ (b v a')) v ((a ^ b') v (a' ^ (a v b')))) = (((b' ^ (b v a')) v (a ^ b')) v (a' ^ (a v b')))
77 ax-a2 31 . . . . . . . . . . . . 13 ((b' ^ (b v a')) v (a ^ b')) = ((a ^ b') v (b' ^ (b v a')))
78 coman2 186 . . . . . . . . . . . . . . . 16 (a ^ b') C b'
7978comcom 453 . . . . . . . . . . . . . . 15 b' C (a ^ b')
8079, 43fh4 472 . . . . . . . . . . . . . 14 ((a ^ b') v (b' ^ (b v a'))) = (((a ^ b') v b') ^ ((a ^ b') v (b v a')))
81 ax-a2 31 . . . . . . . . . . . . . . . . 17 ((a ^ b') v b') = (b' v (a ^ b'))
82 ancom 74 . . . . . . . . . . . . . . . . . . 19 (a ^ b') = (b' ^ a)
8382lor 70 . . . . . . . . . . . . . . . . . 18 (b' v (a ^ b')) = (b' v (b' ^ a))
84 orabs 120 . . . . . . . . . . . . . . . . . 18 (b' v (b' ^ a)) = b'
8583, 84ax-r2 36 . . . . . . . . . . . . . . . . 17 (b' v (a ^ b')) = b'
8681, 85ax-r2 36 . . . . . . . . . . . . . . . 16 ((a ^ b') v b') = b'
87 ax-a2 31 . . . . . . . . . . . . . . . . . . 19 (b v a') = (a' v b)
88 anor1 88 . . . . . . . . . . . . . . . . . . . . 21 (a ^ b') = (a' v b)'
8988con2 67 . . . . . . . . . . . . . . . . . . . 20 (a ^ b')' = (a' v b)
9089ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (a' v b) = (a ^ b')'
9187, 90ax-r2 36 . . . . . . . . . . . . . . . . . 18 (b v a') = (a ^ b')'
9291lor 70 . . . . . . . . . . . . . . . . 17 ((a ^ b') v (b v a')) = ((a ^ b') v (a ^ b')')
93 df-t 41 . . . . . . . . . . . . . . . . . 18 1 = ((a ^ b') v (a ^ b')')
9493ax-r1 35 . . . . . . . . . . . . . . . . 17 ((a ^ b') v (a ^ b')') = 1
9592, 94ax-r2 36 . . . . . . . . . . . . . . . 16 ((a ^ b') v (b v a')) = 1
9686, 952an 79 . . . . . . . . . . . . . . 15 (((a ^ b') v b') ^ ((a ^ b') v (b v a'))) = (b' ^ 1)
97 an1 106 . . . . . . . . . . . . . . 15 (b' ^ 1) = b'
9896, 97ax-r2 36 . . . . . . . . . . . . . 14 (((a ^ b') v b') ^ ((a ^ b') v (b v a'))) = b'
9980, 98ax-r2 36 . . . . . . . . . . . . 13 ((a ^ b') v (b' ^ (b v a'))) = b'
10077, 99ax-r2 36 . . . . . . . . . . . 12 ((b' ^ (b v a')) v (a ^ b')) = b'
101100ax-r5 38 . . . . . . . . . . 11 (((b' ^ (b v a')) v (a ^ b')) v (a' ^ (a v b'))) = (b' v (a' ^ (a v b')))
10276, 101ax-r2 36 . . . . . . . . . 10 ((b' ^ (b v a')) v ((a ^ b') v (a' ^ (a v b')))) = (b' v (a' ^ (a v b')))
10374, 1022or 72 . . . . . . . . 9 (((b ^ a') v (b ^ a)) v ((b' ^ (b v a')) v ((a ^ b') v (a' ^ (a v b'))))) = (((b ^ a) v (a' ^ b)) v (b' v (a' ^ (a v b'))))
104 or4 84 . . . . . . . . . 10 (((b ^ a) v (a' ^ b)) v (b' v (a' ^ (a v b')))) = (((b ^ a) v b') v ((a' ^ b) v (a' ^ (a v b'))))
105 coman1 185 . . . . . . . . . . . . . . 15 (a' ^ b) C a'
106105comcom 453 . . . . . . . . . . . . . 14 a' C (a' ^ b)
107 comorr 184 . . . . . . . . . . . . . . 15 a C (a v b')
108107comcom3 454 . . . . . . . . . . . . . 14 a' C (a v b')
109106, 108fh4 472 . . . . . . . . . . . . 13 ((a' ^ b) v (a' ^ (a v b'))) = (((a' ^ b) v a') ^ ((a' ^ b) v (a v b')))
110 ax-a2 31 . . . . . . . . . . . . . . . 16 ((a' ^ b) v a') = (a' v (a' ^ b))
111 orabs 120 . . . . . . . . . . . . . . . 16 (a' v (a' ^ b)) = a'
112110, 111ax-r2 36 . . . . . . . . . . . . . . 15 ((a' ^ b) v a') = a'
113 anor2 89 . . . . . . . . . . . . . . . . . . 19 (a' ^ b) = (a v b')'
114113con2 67 . . . . . . . . . . . . . . . . . 18 (a' ^ b)' = (a v b')
115114ax-r1 35 . . . . . . . . . . . . . . . . 17 (a v b') = (a' ^ b)'
116115lor 70 . . . . . . . . . . . . . . . 16 ((a' ^ b) v (a v b')) = ((a' ^ b) v (a' ^ b)')
117 df-t 41 . . . . . . . . . . . . . . . . 17 1 = ((a' ^ b) v (a' ^ b)')
118117ax-r1 35 . . . . . . . . . . . . . . . 16 ((a' ^ b) v (a' ^ b)') = 1
119116, 118ax-r2 36 . . . . . . . . . . . . . . 15 ((a' ^ b) v (a v b')) = 1
120112, 1192an 79 . . . . . . . . . . . . . 14 (((a' ^ b) v a') ^ ((a' ^ b) v (a v b'))) = (a' ^ 1)
121 an1 106 . . . . . . . . . . . . . 14 (a' ^ 1) = a'
122120, 121ax-r2 36 . . . . . . . . . . . . 13 (((a' ^ b) v a') ^ ((a' ^ b) v (a v b'))) = a'
123109, 122ax-r2 36 . . . . . . . . . . . 12 ((a' ^ b) v (a' ^ (a v b'))) = a'
124123lor 70 . . . . . . . . . . 11 (((b ^ a) v b') v ((a' ^ b) v (a' ^ (a v b')))) = (((b ^ a) v b') v a')
125 df-a 40 . . . . . . . . . . . . . . 15 (b ^ a) = (b' v a')'
126125con2 67 . . . . . . . . . . . . . 14 (b ^ a)' = (b' v a')
127126ax-r1 35 . . . . . . . . . . . . 13 (b' v a') = (b ^ a)'
128127lor 70 . . . . . . . . . . . 12 ((b ^ a) v (b' v a')) = ((b ^ a) v (b ^ a)')
129 ax-a3 32 . . . . . . . . . . . 12 (((b ^ a) v b') v a') = ((b ^ a) v (b' v a'))
130 df-t 41 . . . . . . . . . . . 12 1 = ((b ^ a) v (b ^ a)')
131128, 129, 1303tr1 63 . . . . . . . . . . 11 (((b ^ a) v b') v a') = 1
132124, 131ax-r2 36 . . . . . . . . . 10 (((b ^ a) v b') v ((a' ^ b) v (a' ^ (a v b')))) = 1
133104, 132ax-r2 36 . . . . . . . . 9 (((b ^ a) v (a' ^ b)) v (b' v (a' ^ (a v b')))) = 1
134103, 133ax-r2 36 . . . . . . . 8 (((b ^ a') v (b ^ a)) v ((b' ^ (b v a')) v ((a ^ b') v (a' ^ (a v b'))))) = 1
13570, 134ax-r2 36 . . . . . . 7 ((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v ((a ^ b') v (a' ^ (a v b')))) = 1
13669, 1352an 79 . . . . . 6 (((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v (a v b)) ^ ((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v ((a ^ b') v (a' ^ (a v b'))))) = (1 ^ 1)
13719, 136ax-r2 36 . . . . 5 ((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v ((a v b) ^ ((a ^ b') v (a' ^ (a v b'))))) = (1 ^ 1)
1384, 137ax-r2 36 . . . 4 (((a v b) ^ ((a ^ b') v (a' ^ (a v b')))) v (((b ^ a') v (b ^ a)) v (b' ^ (b v a')))) = (1 ^ 1)
1393, 138ax-r2 36 . . 3 ((a ->3 b)' v (b' ->3 a')) = (1 ^ 1)
140139, 63ax-r2 36 . 2 ((a ->3 b)' v (b' ->3 a')) = 1
141140i0i3 512 1 ((a ->3 b) ->3 ((a ->3 b) ->3 (b' ->3 a'))) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8   ->3 wi3 14
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-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator