Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  i3bi GIF version

Theorem i3bi 496
 Description: Kalmbach implication and biconditional.
Assertion
Ref Expression
i3bi ((a3 b) ∩ (b3 a)) = (ab)

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