QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  i3bi Unicode version
Theorem i3bi 496
Description: Kalmbach implication and biconditional.
Assertion
Ref Expression
i3bi ((a ->3 b) ^ (b ->3 a)) = (a == b)
Proof of Theorem i3bi
StepHypRef Expression
1 anor2 89 . . . . . . 7 (b' ^ a) = (b v a')'
2 lea 160 . . . . . . . . . . . . 13 (a' ^ b) =< a'
3 leo 158 . . . . . . . . . . . . . 14 a' =< (a' v b)
4 ax-a2 31 . . . . . . . . . . . . . 14 (a' v b) = (b v a')
53, 4lbtr 139 . . . . . . . . . . . . 13 a' =< (b v a')
62, 5letr 137 . . . . . . . . . . . 12 (a' ^ b) =< (b v a')
7 lea 160 . . . . . . . . . . . . 13 ((a' v b) ^ a) =< (a' v b)
8 ancom 74 . . . . . . . . . . . . 13 (a ^ (a' v b)) = ((a' v b) ^ a)
9 ax-a2 31 . . . . . . . . . . . . 13 (b v a') = (a' v b)
107, 8, 9le3tr1 140 . . . . . . . . . . . 12 (a ^ (a' v b)) =< (b v a')
116, 10le2or 168 . . . . . . . . . . 11 ((a' ^ b) v (a ^ (a' v b))) =< ((b v a') v (b v a'))
12 oridm 110 . . . . . . . . . . 11 ((b v a') v (b v a')) = (b v a')
1311, 12lbtr 139 . . . . . . . . . 10 ((a' ^ b) v (a ^ (a' v b))) =< (b v a')
1413lecom 180 . . . . . . . . 9 ((a' ^ b) v (a ^ (a' v b))) C (b v a')
1514comcom2 183 . . . . . . . 8 ((a' ^ b) v (a ^ (a' v b))) C (b v a')'
1615comcom 453 . . . . . . 7 (b v a')' C ((a' ^ b) v (a ^ (a' v b)))
171, 16bctr 181 . . . . . 6 (b' ^ a) C ((a' ^ b) v (a ^ (a' v b)))
18 lea 160 . . . . . . . . . . 11 (b ^ (b' v a)) =< b
19 leo 158 . . . . . . . . . . 11 b =< (b v a')
2018, 19letr 137 . . . . . . . . . 10 (b ^ (b' v a)) =< (b v a')
2120lecom 180 . . . . . . . . 9 (b ^ (b' v a)) C (b v a')
2221comcom2 183 . . . . . . . 8 (b ^ (b' v a)) C (b v a')'
2322comcom 453 . . . . . . 7 (b v a')' C (b ^ (b' v a))
241, 23bctr 181 . . . . . 6 (b' ^ a) C (b ^ (b' v a))
2517, 24fh2 470 . . . . 5 (((a' ^ b) v (a ^ (a' v b))) ^ ((b' ^ a) v (b ^ (b' v a)))) = ((((a' ^ b) v (a ^ (a' v b))) ^ (b' ^ a)) v (((a' ^ b) v (a ^ (a' v b))) ^ (b ^ (b' v a))))
26 ancom 74 . . . . . . . 8 (((a' ^ b) v (a ^ (a' v b))) ^ (b' ^ a)) = ((b' ^ a) ^ ((a' ^ b) v (a ^ (a' v b))))
27 lea 160 . . . . . . . . . . . . . 14 (b' ^ a) =< b'
28 leo 158 . . . . . . . . . . . . . 14 b' =< (b' v a)
2927, 28letr 137 . . . . . . . . . . . . 13 (b' ^ a) =< (b' v a)
3029lecom 180 . . . . . . . . . . . 12 (b' ^ a) C (b' v a)
3130comcom2 183 . . . . . . . . . . 11 (b' ^ a) C (b' v a)'
32 ancom 74 . . . . . . . . . . . . 13 (a' ^ b) = (b ^ a')
33 anor1 88 . . . . . . . . . . . . 13 (b ^ a') = (b' v a)'
3432, 33ax-r2 36 . . . . . . . . . . . 12 (a' ^ b) = (b' v a)'
3534ax-r1 35 . . . . . . . . . . 11 (b' v a)' = (a' ^ b)
3631, 35cbtr 182 . . . . . . . . . 10 (b' ^ a) C (a' ^ b)
37 ancom 74 . . . . . . . . . . . 12 (b' ^ a) = (a ^ b')
38 anor1 88 . . . . . . . . . . . 12 (a ^ b') = (a' v b)'
3937, 38ax-r2 36 . . . . . . . . . . 11 (b' ^ a) = (a' v b)'
408, 7bltr 138 . . . . . . . . . . . . . 14 (a ^ (a' v b)) =< (a' v b)
4140lecom 180 . . . . . . . . . . . . 13 (a ^ (a' v b)) C (a' v b)
4241comcom2 183 . . . . . . . . . . . 12 (a ^ (a' v b)) C (a' v b)'
4342comcom 453 . . . . . . . . . . 11 (a' v b)' C (a ^ (a' v b))
4439, 43bctr 181 . . . . . . . . . 10 (b' ^ a) C (a ^ (a' v b))
4536, 44fh1 469 . . . . . . . . 9 ((b' ^ a) ^ ((a' ^ b) v (a ^ (a' v b)))) = (((b' ^ a) ^ (a' ^ b)) v ((b' ^ a) ^ (a ^ (a' v b))))
4637ran 78 . . . . . . . . . . . 12 ((b' ^ a) ^ (a' ^ b)) = ((a ^ b') ^ (a' ^ b))
47 an4 86 . . . . . . . . . . . . 13 ((a ^ b') ^ (a' ^ b)) = ((a ^ a') ^ (b' ^ b))
48 dff 101 . . . . . . . . . . . . . . . 16 0 = (a ^ a')
49 dff 101 . . . . . . . . . . . . . . . . 17 0 = (b ^ b')
50 ancom 74 . . . . . . . . . . . . . . . . 17 (b ^ b') = (b' ^ b)
5149, 50ax-r2 36 . . . . . . . . . . . . . . . 16 0 = (b' ^ b)
5248, 512an 79 . . . . . . . . . . . . . . 15 (0 ^ 0) = ((a ^ a') ^ (b' ^ b))
5352ax-r1 35 . . . . . . . . . . . . . 14 ((a ^ a') ^ (b' ^ b)) = (0 ^ 0)
54 anidm 111 . . . . . . . . . . . . . 14 (0 ^ 0) = 0
5553, 54ax-r2 36 . . . . . . . . . . . . 13 ((a ^ a') ^ (b' ^ b)) = 0
5647, 55ax-r2 36 . . . . . . . . . . . 12 ((a ^ b') ^ (a' ^ b)) = 0
5746, 56ax-r2 36 . . . . . . . . . . 11 ((b' ^ a) ^ (a' ^ b)) = 0
58 an12 81 . . . . . . . . . . . 12 ((b' ^ a) ^ (a ^ (a' v b))) = (a ^ ((b' ^ a) ^ (a' v b)))
59 dff 101 . . . . . . . . . . . . . . . 16 0 = ((b' ^ a) ^ (b' ^ a)')
601con2 67 . . . . . . . . . . . . . . . . . 18 (b' ^ a)' = (b v a')
6160, 9ax-r2 36 . . . . . . . . . . . . . . . . 17 (b' ^ a)' = (a' v b)
6261lan 77 . . . . . . . . . . . . . . . 16 ((b' ^ a) ^ (b' ^ a)') = ((b' ^ a) ^ (a' v b))
6359, 62ax-r2 36 . . . . . . . . . . . . . . 15 0 = ((b' ^ a) ^ (a' v b))
6463lan 77 . . . . . . . . . . . . . 14 (a ^ 0) = (a ^ ((b' ^ a) ^ (a' v b)))
6564ax-r1 35 . . . . . . . . . . . . 13 (a ^ ((b' ^ a) ^ (a' v b))) = (a ^ 0)
66 an0 108 . . . . . . . . . . . . 13 (a ^ 0) = 0
6765, 66ax-r2 36 . . . . . . . . . . . 12 (a ^ ((b' ^ a) ^ (a' v b))) = 0
6858, 67ax-r2 36 . . . . . . . . . . 11 ((b' ^ a) ^ (a ^ (a' v b))) = 0
6957, 682or 72 . . . . . . . . . 10 (((b' ^ a) ^ (a' ^ b)) v ((b' ^ a) ^ (a ^ (a' v b)))) = (0 v 0)
70 oridm 110 . . . . . . . . . 10 (0 v 0) = 0
7169, 70ax-r2 36 . . . . . . . . 9 (((b' ^ a) ^ (a' ^ b)) v ((b' ^ a) ^ (a ^ (a' v b)))) = 0
7245, 71ax-r2 36 . . . . . . . 8 ((b' ^ a) ^ ((a' ^ b) v (a ^ (a' v b)))) = 0
7326, 72ax-r2 36 . . . . . . 7 (((a' ^ b) v (a ^ (a' v b))) ^ (b' ^ a)) = 0
74 ancom 74 . . . . . . . 8 (((a' ^ b) v (a ^ (a' v b))) ^ (b ^ (b' v a))) = ((b ^ (b' v a)) ^ ((a' ^ b) v (a ^ (a' v b))))
75 ancom 74 . . . . . . . . . . . . . . 15 (b ^ (b' v a)) = ((b' v a) ^ b)
76 lea 160 . . . . . . . . . . . . . . 15 ((b' v a) ^ b) =< (b' v a)
7775, 76bltr 138 . . . . . . . . . . . . . 14 (b ^ (b' v a)) =< (b' v a)
7877lecom 180 . . . . . . . . . . . . 13 (b ^ (b' v a)) C (b' v a)
7978comcom2 183 . . . . . . . . . . . 12 (b ^ (b' v a)) C (b' v a)'
8079comcom 453 . . . . . . . . . . 11 (b' v a)' C (b ^ (b' v a))
8134, 80bctr 181 . . . . . . . . . 10 (a' ^ b) C (b ^ (b' v a))
82 anor2 89 . . . . . . . . . . 11 (a' ^ b) = (a v b')'
83 lea 160 . . . . . . . . . . . . . . 15 (a ^ (a' v b)) =< a
84 leo 158 . . . . . . . . . . . . . . 15 a =< (a v b')
8583, 84letr 137 . . . . . . . . . . . . . 14 (a ^ (a' v b)) =< (a v b')
8685lecom 180 . . . . . . . . . . . . 13 (a ^ (a' v b)) C (a v b')
8786comcom2 183 . . . . . . . . . . . 12 (a ^ (a' v b)) C (a v b')'
8887comcom 453 . . . . . . . . . . 11 (a v b')' C (a ^ (a' v b))
8982, 88bctr 181 . . . . . . . . . 10 (a' ^ b) C (a ^ (a' v b))
9081, 89fh2 470 . . . . . . . . 9 ((b ^ (b' v a)) ^ ((a' ^ b) v (a ^ (a' v b)))) = (((b ^ (b' v a)) ^ (a' ^ b)) v ((b ^ (b' v a)) ^ (a ^ (a' v b))))
91 ax-a2 31 . . . . . . . . . 10 (((b ^ (b' v a)) ^ (a' ^ b)) v ((b ^ (b' v a)) ^ (a ^ (a' v b)))) = (((b ^ (b' v a)) ^ (a ^ (a' v b))) v ((b ^ (b' v a)) ^ (a' ^ b)))
92 an4 86 . . . . . . . . . . . . 13 ((b ^ (b' v a)) ^ (a ^ (a' v b))) = ((b ^ a) ^ ((b' v a) ^ (a' v b)))
93 anandi 114 . . . . . . . . . . . . . 14 ((b ^ a) ^ ((b' v a) ^ (a' v b))) = (((b ^ a) ^ (b' v a)) ^ ((b ^ a) ^ (a' v b)))
94 coman1 185 . . . . . . . . . . . . . . . . . . 19 (b ^ a) C b
9594comcom2 183 . . . . . . . . . . . . . . . . . 18 (b ^ a) C b'
96 ancom 74 . . . . . . . . . . . . . . . . . . 19 (b ^ a) = (a ^ b)
97 coman1 185 . . . . . . . . . . . . . . . . . . 19 (a ^ b) C a
9896, 97bctr 181 . . . . . . . . . . . . . . . . . 18 (b ^ a) C a
9995, 98fh1 469 . . . . . . . . . . . . . . . . 17 ((b ^ a) ^ (b' v a)) = (((b ^ a) ^ b') v ((b ^ a) ^ a))
100 an32 83 . . . . . . . . . . . . . . . . . . . . 21 ((b ^ a) ^ b') = ((b ^ b') ^ a)
101 ancom 74 . . . . . . . . . . . . . . . . . . . . . 22 ((b ^ b') ^ a) = (a ^ (b ^ b'))
10249lan 77 . . . . . . . . . . . . . . . . . . . . . . . 24 (a ^ 0) = (a ^ (b ^ b'))
103102ax-r1 35 . . . . . . . . . . . . . . . . . . . . . . 23 (a ^ (b ^ b')) = (a ^ 0)
104103, 66ax-r2 36 . . . . . . . . . . . . . . . . . . . . . 22 (a ^ (b ^ b')) = 0
105101, 104ax-r2 36 . . . . . . . . . . . . . . . . . . . . 21 ((b ^ b') ^ a) = 0
106100, 105ax-r2 36 . . . . . . . . . . . . . . . . . . . 20 ((b ^ a) ^ b') = 0
107 anass 76 . . . . . . . . . . . . . . . . . . . . 21 ((b ^ a) ^ a) = (b ^ (a ^ a))
108 anidm 111 . . . . . . . . . . . . . . . . . . . . . 22 (a ^ a) = a
109108lan 77 . . . . . . . . . . . . . . . . . . . . 21 (b ^ (a ^ a)) = (b ^ a)
110107, 109ax-r2 36 . . . . . . . . . . . . . . . . . . . 20 ((b ^ a) ^ a) = (b ^ a)
111106, 1102or 72 . . . . . . . . . . . . . . . . . . 19 (((b ^ a) ^ b') v ((b ^ a) ^ a)) = (0 v (b ^ a))
112 ax-a2 31 . . . . . . . . . . . . . . . . . . 19 (0 v (b ^ a)) = ((b ^ a) v 0)
113111, 112ax-r2 36 . . . . . . . . . . . . . . . . . 18 (((b ^ a) ^ b') v ((b ^ a) ^ a)) = ((b ^ a) v 0)
114 or0 102 . . . . . . . . . . . . . . . . . 18 ((b ^ a) v 0) = (b ^ a)
115113, 114ax-r2 36 . . . . . . . . . . . . . . . . 17 (((b ^ a) ^ b') v ((b ^ a) ^ a)) = (b ^ a)
11699, 115ax-r2 36 . . . . . . . . . . . . . . . 16 ((b ^ a) ^ (b' v a)) = (b ^ a)
11798comcom2 183 . . . . . . . . . . . . . . . . . 18 (b ^ a) C a'
118117, 94fh1 469 . . . . . . . . . . . . . . . . 17 ((b ^ a) ^ (a' v b)) = (((b ^ a) ^ a') v ((b ^ a) ^ b))
119 anass 76 . . . . . . . . . . . . . . . . . . . . 21 ((b ^ a) ^ a') = (b ^ (a ^ a'))
12048lan 77 . . . . . . . . . . . . . . . . . . . . . . 23 (b ^ 0) = (b ^ (a ^ a'))
121120ax-r1 35 . . . . . . . . . . . . . . . . . . . . . 22 (b ^ (a ^ a')) = (b ^ 0)
122 an0 108 . . . . . . . . . . . . . . . . . . . . . 22 (b ^ 0) = 0
123121, 122ax-r2 36 . . . . . . . . . . . . . . . . . . . . 21 (b ^ (a ^ a')) = 0
124119, 123ax-r2 36 . . . . . . . . . . . . . . . . . . . 20 ((b ^ a) ^ a') = 0
125 an32 83 . . . . . . . . . . . . . . . . . . . . 21 ((b ^ a) ^ b) = ((b ^ b) ^ a)
126 anidm 111 . . . . . . . . . . . . . . . . . . . . . 22 (b ^ b) = b
127126ran 78 . . . . . . . . . . . . . . . . . . . . 21 ((b ^ b) ^ a) = (b ^ a)
128125, 127ax-r2 36 . . . . . . . . . . . . . . . . . . . 20 ((b ^ a) ^ b) = (b ^ a)
129124, 1282or 72 . . . . . . . . . . . . . . . . . . 19 (((b ^ a) ^ a') v ((b ^ a) ^ b)) = (0 v (b ^ a))
130129, 112ax-r2 36 . . . . . . . . . . . . . . . . . 18 (((b ^ a) ^ a') v ((b ^ a) ^ b)) = ((b ^ a) v 0)
131130, 114ax-r2 36 . . . . . . . . . . . . . . . . 17 (((b ^ a) ^ a') v ((b ^ a) ^ b)) = (b ^ a)
132118, 131ax-r2 36 . . . . . . . . . . . . . . . 16 ((b ^ a) ^ (a' v b)) = (b ^ a)
133116, 1322an 79 . . . . . . . . . . . . . . 15 (((b ^ a) ^ (b' v a)) ^ ((b ^ a) ^ (a' v b))) = ((b ^ a) ^ (b ^ a))
134 anidm 111 . . . . . . . . . . . . . . . 16 ((b ^ a) ^ (b ^ a)) = (b ^ a)
135134, 96ax-r2 36 . . . . . . . . . . . . . . 15 ((b ^ a) ^ (b ^ a)) = (a ^ b)
136133, 135ax-r2 36 . . . . . . . . . . . . . 14 (((b ^ a) ^ (b' v a)) ^ ((b ^ a) ^ (a' v b))) = (a ^ b)
13793, 136ax-r2 36 . . . . . . . . . . . . 13 ((b ^ a) ^ ((b' v a) ^ (a' v b))) = (a ^ b)
13892, 137ax-r2 36 . . . . . . . . . . . 12 ((b ^ (b' v a)) ^ (a ^ (a' v b))) = (a ^ b)
139 anass 76 . . . . . . . . . . . . . 14 ((b ^ (b' v a)) ^ (a' ^ b)) = (b ^ ((b' v a) ^ (a' ^ b)))
140 dff 101 . . . . . . . . . . . . . . . . 17 0 = ((b' v a) ^ (b' v a)')
14135lan 77 . . . . . . . . . . . . . . . . 17 ((b' v a) ^ (b' v a)') = ((b' v a) ^ (a' ^ b))
142140, 141ax-r2 36 . . . . . . . . . . . . . . . 16 0 = ((b' v a) ^ (a' ^ b))
143142lan 77 . . . . . . . . . . . . . . 15 (b ^ 0) = (b ^ ((b' v a) ^ (a' ^ b)))
144143ax-r1 35 . . . . . . . . . . . . . 14 (b ^ ((b' v a) ^ (a' ^ b))) = (b ^ 0)
145139, 144ax-r2 36 . . . . . . . . . . . . 13 ((b ^ (b' v a)) ^ (a' ^ b)) = (b ^ 0)
146145, 122ax-r2 36 . . . . . . . . . . . 12 ((b ^ (b' v a)) ^ (a' ^ b)) = 0
147138, 1462or 72 . . . . . . . . . . 11 (((b ^ (b' v a)) ^ (a ^ (a' v b))) v ((b ^ (b' v a)) ^ (a' ^ b))) = ((a ^ b) v 0)
148 or0 102 . . . . . . . . . . 11 ((a ^ b) v 0) = (a ^ b)
149147, 148ax-r2 36 . . . . . . . . . 10 (((b ^ (b' v a)) ^ (a ^ (a' v b))) v ((b ^ (b' v a)) ^ (a' ^ b))) = (a ^ b)
15091, 149ax-r2 36 . . . . . . . . 9 (((b ^ (b' v a)) ^ (a' ^ b)) v ((b ^ (b' v a)) ^ (a ^ (a' v b)))) = (a ^ b)
15190, 150ax-r2 36 . . . . . . . 8 ((b ^ (b' v a)) ^ ((a' ^ b) v (a ^ (a' v b)))) = (a ^ b)
15274, 151ax-r2 36 . . . . . . 7 (((a' ^ b) v (a ^ (a' v b))) ^ (b ^ (b' v a))) = (a ^ b)
15373, 1522or 72 . . . . . 6 ((((a' ^ b) v (a ^ (a' v b))) ^ (b' ^ a)) v (((a' ^ b) v (a ^ (a' v b))) ^ (b ^ (b' v a)))) = (0 v (a ^ b))
154 ax-a2 31 . . . . . . 7 (0 v (a ^ b)) = ((a ^ b) v 0)
155154, 148ax-r2 36 . . . . . 6 (0 v (a ^ b)) = (a ^ b)
156153, 155ax-r2 36 . . . . 5 ((((a' ^ b) v (a ^ (a' v b))) ^ (b' ^ a)) v (((a' ^ b) v (a ^ (a' v b))) ^ (b ^ (b' v a)))) = (a ^ b)
15725, 156ax-r2 36 . . . 4 (((a' ^ b) v (a ^ (a' v b))) ^ ((b' ^ a) v (b ^ (b' v a)))) = (a ^ b)
158157lor 70 . . 3 ((a' ^ b') v (((a' ^ b) v (a ^ (a' v b))) ^ ((b' ^ a) v (b ^ (b' v a))))) = ((a' ^ b') v (a ^ b))
159 ancom 74 . . . . . 6 (a' ^ b') = (b' ^ a')
160 oran 87 . . . . . . . 8 (b v a) = (b' ^ a')'
161160ax-r1 35 . . . . . . 7 (b' ^ a')' = (b v a)
162161con3 68 . . . . . 6 (b' ^ a') = (b v a)'
163159, 162ax-r2 36 . . . . 5 (a' ^ b') = (b v a)'
164 lea 160 . . . . . . . . . 10 (b ^ a') =< b
16532, 164bltr 138 . . . . . . . . 9 (a' ^ b) =< b
166165, 83le2or 168 . . . . . . . 8 ((a' ^ b) v (a ^ (a' v b))) =< (b v a)
167166lecom 180 . . . . . . 7 ((a' ^ b) v (a ^ (a' v b))) C (b v a)
168167comcom2 183 . . . . . 6 ((a' ^ b) v (a ^ (a' v b))) C (b v a)'
169168comcom 453 . . . . 5 (b v a)' C ((a' ^ b) v (a ^ (a' v b)))
170163, 169bctr 181 . . . 4 (a' ^ b') C ((a' ^ b) v (a ^ (a' v b)))
171 oran 87 . . . . . . 7 (a v b) = (a' ^ b')'
172171ax-r1 35 . . . . . 6 (a' ^ b')' = (a v b)
173172con3 68 . . . . 5 (a' ^ b') = (a v b)'
174 lea 160 . . . . . . . . . 10 (a ^ b') =< a
17537, 174bltr 138 . . . . . . . . 9 (b' ^ a) =< a
176175, 18le2or 168 . . . . . . . 8 ((b' ^ a) v (b ^ (b' v a))) =< (a v b)
177176lecom 180 . . . . . . 7 ((b' ^ a) v (b ^ (b' v a))) C (a v b)
178177comcom2 183 . . . . . 6 ((b' ^ a) v (b ^ (b' v a))) C (a v b)'
179178comcom 453 . . . . 5 (a v b)' C ((b' ^ a) v (b ^ (b' v a)))
180173, 179bctr 181 . . . 4 (a' ^ b') C ((b' ^ a) v (b ^ (b' v a)))
181170, 180fh3 471 . . 3 ((a' ^ b') v (((a' ^ b) v (a ^ (a' v b))) ^ ((b' ^ a) v (b ^ (b' v a))))) = (((a' ^ b') v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a' ^ b') v ((b' ^ a) v (b ^ (b' v a)))))
182 ax-a2 31 . . 3 ((a' ^ b') v (a ^ b)) = ((a ^ b) v (a' ^ b'))
183158, 181, 1823tr2 64 . 2 (((a' ^ b') v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a' ^ b') v ((b' ^ a) v (b ^ (b' v a))))) = ((a ^ b) v (a' ^ b'))
184 df-i3 46 . . . 4 (a ->3 b) = (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))
185 or32 82 . . . . 5 (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))) = (((a' ^ b) v (a ^ (a' v b))) v (a' ^ b'))
186 ax-a2 31 . . . . 5 (((a' ^ b) v (a ^ (a' v b))) v (a' ^ b')) = ((a' ^ b') v ((a' ^ b) v (a ^ (a' v b))))
187185, 186ax-r2 36 . . . 4 (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))) = ((a' ^ b') v ((a' ^ b) v (a ^ (a' v b))))
188184, 187ax-r2 36 . . 3 (a ->3 b) = ((a' ^ b') v ((a' ^ b) v (a ^ (a' v b))))
189 df-i3 46 . . . 4 (b ->3 a) = (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))
190 or32 82 . . . . 5 (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))) = (((b' ^ a) v (b ^ (b' v a))) v (b' ^ a'))
191 ancom 74 . . . . . . 7 (b' ^ a') = (a' ^ b')
192191lor 70 . . . . . 6 (((b' ^ a) v (b ^ (b' v a))) v (b' ^ a')) = (((b' ^ a) v (b ^ (b' v a))) v (a' ^ b'))
193 ax-a2 31 . . . . . 6 (((b' ^ a) v (b ^ (b' v a))) v (a' ^ b')) = ((a' ^ b') v ((b' ^ a) v (b ^ (b' v a))))
194192, 193ax-r2 36 . . . . 5 (((b' ^ a) v (b ^ (b' v a))) v (b' ^ a')) = ((a' ^ b') v ((b' ^ a) v (b ^ (b' v a))))
195190, 194ax-r2 36 . . . 4 (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))) = ((a' ^ b') v ((b' ^ a) v (b ^ (b' v a))))
196189, 195ax-r2 36 . . 3 (b ->3 a) = ((a' ^ b') v ((b' ^ a) v (b ^ (b' v a))))
197188, 1962an 79 . 2 ((a ->3 b) ^ (b ->3 a)) = (((a' ^ b') v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a' ^ b') v ((b' ^ a) v (b ^ (b' v a)))))
198 dfb 94 . 2 (a == b) = ((a ^ b) v (a' ^ b'))
199183, 197, 1983tr1 63 1 ((a ->3 b) ^ (b ->3 a)) = (a == b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  0wf 9   ->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:  i3or  497  bii3  516  u3lembi  723
  Copyright terms: Public domain W3C validator