QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud5lem1a Unicode version
Theorem ud5lem1a 586
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud5lem1a ((a ->5 b) ^ (b ->5 a)) = ((a ^ b) v (a' ^ b'))
Proof of Theorem ud5lem1a
StepHypRef Expression
1 df-i5 48 . . 3 (a ->5 b) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))
2 df-i5 48 . . 3 (b ->5 a) = (((b ^ a) v (b' ^ a)) v (b' ^ a'))
31, 22an 79 . 2 ((a ->5 b) ^ (b ->5 a)) = ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (((b ^ a) v (b' ^ a)) v (b' ^ a')))
4 ax-a2 31 . . . 4 (((b ^ a) v (b' ^ a)) v (b' ^ a')) = ((b' ^ a') v ((b ^ a) v (b' ^ a)))
54lan 77 . . 3 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (((b ^ a) v (b' ^ a)) v (b' ^ a'))) = ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b' ^ a') v ((b ^ a) v (b' ^ a))))
6 coman2 186 . . . . . . . . . 10 (a ^ b) C b
76comcom2 183 . . . . . . . . 9 (a ^ b) C b'
8 coman1 185 . . . . . . . . . 10 (a ^ b) C a
98comcom2 183 . . . . . . . . 9 (a ^ b) C a'
107, 9com2an 484 . . . . . . . 8 (a ^ b) C (b' ^ a')
1110comcom 453 . . . . . . 7 (b' ^ a') C (a ^ b)
12 coman2 186 . . . . . . . . . 10 (a' ^ b) C b
1312comcom2 183 . . . . . . . . 9 (a' ^ b) C b'
14 coman1 185 . . . . . . . . 9 (a' ^ b) C a'
1513, 14com2an 484 . . . . . . . 8 (a' ^ b) C (b' ^ a')
1615comcom 453 . . . . . . 7 (b' ^ a') C (a' ^ b)
1711, 16com2or 483 . . . . . 6 (b' ^ a') C ((a ^ b) v (a' ^ b))
18 coman2 186 . . . . . . 7 (b' ^ a') C a'
19 coman1 185 . . . . . . 7 (b' ^ a') C b'
2018, 19com2an 484 . . . . . 6 (b' ^ a') C (a' ^ b')
2117, 20com2or 483 . . . . 5 (b' ^ a') C (((a ^ b) v (a' ^ b)) v (a' ^ b'))
22 coman1 185 . . . . . . . . 9 (b ^ a) C b
2322comcom2 183 . . . . . . . 8 (b ^ a) C b'
24 coman2 186 . . . . . . . . 9 (b ^ a) C a
2524comcom2 183 . . . . . . . 8 (b ^ a) C a'
2623, 25com2an 484 . . . . . . 7 (b ^ a) C (b' ^ a')
2726comcom 453 . . . . . 6 (b' ^ a') C (b ^ a)
28 coman1 185 . . . . . . . 8 (b' ^ a) C b'
29 coman2 186 . . . . . . . . 9 (b' ^ a) C a
3029comcom2 183 . . . . . . . 8 (b' ^ a) C a'
3128, 30com2an 484 . . . . . . 7 (b' ^ a) C (b' ^ a')
3231comcom 453 . . . . . 6 (b' ^ a') C (b' ^ a)
3327, 32com2or 483 . . . . 5 (b' ^ a') C ((b ^ a) v (b' ^ a))
3421, 33fh2 470 . . . 4 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b' ^ a') v ((b ^ a) v (b' ^ a)))) = (((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a')) v ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b ^ a) v (b' ^ a))))
3518comcom3 454 . . . . . . . . . . 11 (b' ^ a')' C a'
3635comcom5 458 . . . . . . . . . 10 (b' ^ a') C a
3719comcom3 454 . . . . . . . . . . 11 (b' ^ a')' C b'
3837comcom5 458 . . . . . . . . . 10 (b' ^ a') C b
3936, 38com2an 484 . . . . . . . . 9 (b' ^ a') C (a ^ b)
4018, 38com2an 484 . . . . . . . . 9 (b' ^ a') C (a' ^ b)
4139, 40com2or 483 . . . . . . . 8 (b' ^ a') C ((a ^ b) v (a' ^ b))
4241, 20fh1r 473 . . . . . . 7 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a')) = ((((a ^ b) v (a' ^ b)) ^ (b' ^ a')) v ((a' ^ b') ^ (b' ^ a')))
4311, 16fh1r 473 . . . . . . . . . 10 (((a ^ b) v (a' ^ b)) ^ (b' ^ a')) = (((a ^ b) ^ (b' ^ a')) v ((a' ^ b) ^ (b' ^ a')))
44 anass 76 . . . . . . . . . . . . 13 ((a ^ b) ^ (b' ^ a')) = (a ^ (b ^ (b' ^ a')))
45 anass 76 . . . . . . . . . . . . . . . 16 ((b ^ b') ^ a') = (b ^ (b' ^ a'))
4645ax-r1 35 . . . . . . . . . . . . . . 15 (b ^ (b' ^ a')) = ((b ^ b') ^ a')
4746lan 77 . . . . . . . . . . . . . 14 (a ^ (b ^ (b' ^ a'))) = (a ^ ((b ^ b') ^ a'))
48 ancom 74 . . . . . . . . . . . . . . . . 17 ((b ^ b') ^ a') = (a' ^ (b ^ b'))
49 dff 101 . . . . . . . . . . . . . . . . . . . 20 0 = (b ^ b')
5049ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (b ^ b') = 0
5150lan 77 . . . . . . . . . . . . . . . . . 18 (a' ^ (b ^ b')) = (a' ^ 0)
52 an0 108 . . . . . . . . . . . . . . . . . 18 (a' ^ 0) = 0
5351, 52ax-r2 36 . . . . . . . . . . . . . . . . 17 (a' ^ (b ^ b')) = 0
5448, 53ax-r2 36 . . . . . . . . . . . . . . . 16 ((b ^ b') ^ a') = 0
5554lan 77 . . . . . . . . . . . . . . 15 (a ^ ((b ^ b') ^ a')) = (a ^ 0)
56 an0 108 . . . . . . . . . . . . . . 15 (a ^ 0) = 0
5755, 56ax-r2 36 . . . . . . . . . . . . . 14 (a ^ ((b ^ b') ^ a')) = 0
5847, 57ax-r2 36 . . . . . . . . . . . . 13 (a ^ (b ^ (b' ^ a'))) = 0
5944, 58ax-r2 36 . . . . . . . . . . . 12 ((a ^ b) ^ (b' ^ a')) = 0
60 anass 76 . . . . . . . . . . . . 13 ((a' ^ b) ^ (b' ^ a')) = (a' ^ (b ^ (b' ^ a')))
6146lan 77 . . . . . . . . . . . . . 14 (a' ^ (b ^ (b' ^ a'))) = (a' ^ ((b ^ b') ^ a'))
6254lan 77 . . . . . . . . . . . . . . 15 (a' ^ ((b ^ b') ^ a')) = (a' ^ 0)
6362, 52ax-r2 36 . . . . . . . . . . . . . 14 (a' ^ ((b ^ b') ^ a')) = 0
6461, 63ax-r2 36 . . . . . . . . . . . . 13 (a' ^ (b ^ (b' ^ a'))) = 0
6560, 64ax-r2 36 . . . . . . . . . . . 12 ((a' ^ b) ^ (b' ^ a')) = 0
6659, 652or 72 . . . . . . . . . . 11 (((a ^ b) ^ (b' ^ a')) v ((a' ^ b) ^ (b' ^ a'))) = (0 v 0)
67 or0 102 . . . . . . . . . . 11 (0 v 0) = 0
6866, 67ax-r2 36 . . . . . . . . . 10 (((a ^ b) ^ (b' ^ a')) v ((a' ^ b) ^ (b' ^ a'))) = 0
6943, 68ax-r2 36 . . . . . . . . 9 (((a ^ b) v (a' ^ b)) ^ (b' ^ a')) = 0
70 ancom 74 . . . . . . . . . . 11 (b' ^ a') = (a' ^ b')
7170lan 77 . . . . . . . . . 10 ((a' ^ b') ^ (b' ^ a')) = ((a' ^ b') ^ (a' ^ b'))
72 anidm 111 . . . . . . . . . 10 ((a' ^ b') ^ (a' ^ b')) = (a' ^ b')
7371, 72ax-r2 36 . . . . . . . . 9 ((a' ^ b') ^ (b' ^ a')) = (a' ^ b')
7469, 732or 72 . . . . . . . 8 ((((a ^ b) v (a' ^ b)) ^ (b' ^ a')) v ((a' ^ b') ^ (b' ^ a'))) = (0 v (a' ^ b'))
75 ax-a2 31 . . . . . . . . 9 (0 v (a' ^ b')) = ((a' ^ b') v 0)
76 or0 102 . . . . . . . . 9 ((a' ^ b') v 0) = (a' ^ b')
7775, 76ax-r2 36 . . . . . . . 8 (0 v (a' ^ b')) = (a' ^ b')
7874, 77ax-r2 36 . . . . . . 7 ((((a ^ b) v (a' ^ b)) ^ (b' ^ a')) v ((a' ^ b') ^ (b' ^ a'))) = (a' ^ b')
7942, 78ax-r2 36 . . . . . 6 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a')) = (a' ^ b')
8024, 22com2an 484 . . . . . . . . . 10 (b ^ a) C (a ^ b)
8125, 22com2an 484 . . . . . . . . . 10 (b ^ a) C (a' ^ b)
8280, 81com2or 483 . . . . . . . . 9 (b ^ a) C ((a ^ b) v (a' ^ b))
8325, 23com2an 484 . . . . . . . . 9 (b ^ a) C (a' ^ b')
8482, 83com2or 483 . . . . . . . 8 (b ^ a) C (((a ^ b) v (a' ^ b)) v (a' ^ b'))
8523, 24com2an 484 . . . . . . . 8 (b ^ a) C (b' ^ a)
8684, 85fh2 470 . . . . . . 7 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b ^ a) v (b' ^ a))) = (((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b ^ a)) v ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a)))
8782, 83fh1r 473 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b ^ a)) = ((((a ^ b) v (a' ^ b)) ^ (b ^ a)) v ((a' ^ b') ^ (b ^ a)))
88 anass 76 . . . . . . . . . . . . 13 ((a' ^ b') ^ (b ^ a)) = (a' ^ (b' ^ (b ^ a)))
89 an12 81 . . . . . . . . . . . . . . . . 17 (b ^ (b' ^ a)) = (b' ^ (b ^ a))
9089ax-r1 35 . . . . . . . . . . . . . . . 16 (b' ^ (b ^ a)) = (b ^ (b' ^ a))
91 anass 76 . . . . . . . . . . . . . . . . . 18 ((b ^ b') ^ a) = (b ^ (b' ^ a))
9291ax-r1 35 . . . . . . . . . . . . . . . . 17 (b ^ (b' ^ a)) = ((b ^ b') ^ a)
93 ancom 74 . . . . . . . . . . . . . . . . . 18 ((b ^ b') ^ a) = (a ^ (b ^ b'))
9450lan 77 . . . . . . . . . . . . . . . . . . 19 (a ^ (b ^ b')) = (a ^ 0)
9594, 56ax-r2 36 . . . . . . . . . . . . . . . . . 18 (a ^ (b ^ b')) = 0
9693, 95ax-r2 36 . . . . . . . . . . . . . . . . 17 ((b ^ b') ^ a) = 0
9792, 96ax-r2 36 . . . . . . . . . . . . . . . 16 (b ^ (b' ^ a)) = 0
9890, 97ax-r2 36 . . . . . . . . . . . . . . 15 (b' ^ (b ^ a)) = 0
9998lan 77 . . . . . . . . . . . . . 14 (a' ^ (b' ^ (b ^ a))) = (a' ^ 0)
10099, 52ax-r2 36 . . . . . . . . . . . . 13 (a' ^ (b' ^ (b ^ a))) = 0
10188, 100ax-r2 36 . . . . . . . . . . . 12 ((a' ^ b') ^ (b ^ a)) = 0
102101lor 70 . . . . . . . . . . 11 ((((a ^ b) v (a' ^ b)) ^ (b ^ a)) v ((a' ^ b') ^ (b ^ a))) = ((((a ^ b) v (a' ^ b)) ^ (b ^ a)) v 0)
103 or0 102 . . . . . . . . . . 11 ((((a ^ b) v (a' ^ b)) ^ (b ^ a)) v 0) = (((a ^ b) v (a' ^ b)) ^ (b ^ a))
104102, 103ax-r2 36 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b)) ^ (b ^ a)) v ((a' ^ b') ^ (b ^ a))) = (((a ^ b) v (a' ^ b)) ^ (b ^ a))
10587, 104ax-r2 36 . . . . . . . . 9 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b ^ a)) = (((a ^ b) v (a' ^ b)) ^ (b ^ a))
10628comcom3 454 . . . . . . . . . . . . . 14 (b' ^ a)' C b'
107106comcom5 458 . . . . . . . . . . . . 13 (b' ^ a) C b
10829, 107com2an 484 . . . . . . . . . . . 12 (b' ^ a) C (a ^ b)
10930, 107com2an 484 . . . . . . . . . . . 12 (b' ^ a) C (a' ^ b)
110108, 109com2or 483 . . . . . . . . . . 11 (b' ^ a) C ((a ^ b) v (a' ^ b))
11130, 28com2an 484 . . . . . . . . . . 11 (b' ^ a) C (a' ^ b')
112110, 111fh1r 473 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a)) = ((((a ^ b) v (a' ^ b)) ^ (b' ^ a)) v ((a' ^ b') ^ (b' ^ a)))
113 ancom 74 . . . . . . . . . . . . 13 ((a' ^ b') ^ (b' ^ a)) = ((b' ^ a) ^ (a' ^ b'))
114 anass 76 . . . . . . . . . . . . . 14 ((b' ^ a) ^ (a' ^ b')) = (b' ^ (a ^ (a' ^ b')))
115 anass 76 . . . . . . . . . . . . . . . . . 18 ((a ^ a') ^ b') = (a ^ (a' ^ b'))
116115ax-r1 35 . . . . . . . . . . . . . . . . 17 (a ^ (a' ^ b')) = ((a ^ a') ^ b')
117 ancom 74 . . . . . . . . . . . . . . . . . 18 ((a ^ a') ^ b') = (b' ^ (a ^ a'))
118 dff 101 . . . . . . . . . . . . . . . . . . . . 21 0 = (a ^ a')
119118ax-r1 35 . . . . . . . . . . . . . . . . . . . 20 (a ^ a') = 0
120119lan 77 . . . . . . . . . . . . . . . . . . 19 (b' ^ (a ^ a')) = (b' ^ 0)
121 an0 108 . . . . . . . . . . . . . . . . . . 19 (b' ^ 0) = 0
122120, 121ax-r2 36 . . . . . . . . . . . . . . . . . 18 (b' ^ (a ^ a')) = 0
123117, 122ax-r2 36 . . . . . . . . . . . . . . . . 17 ((a ^ a') ^ b') = 0
124116, 123ax-r2 36 . . . . . . . . . . . . . . . 16 (a ^ (a' ^ b')) = 0
125124lan 77 . . . . . . . . . . . . . . 15 (b' ^ (a ^ (a' ^ b'))) = (b' ^ 0)
126125, 121ax-r2 36 . . . . . . . . . . . . . 14 (b' ^ (a ^ (a' ^ b'))) = 0
127114, 126ax-r2 36 . . . . . . . . . . . . 13 ((b' ^ a) ^ (a' ^ b')) = 0
128113, 127ax-r2 36 . . . . . . . . . . . 12 ((a' ^ b') ^ (b' ^ a)) = 0
129128lor 70 . . . . . . . . . . 11 ((((a ^ b) v (a' ^ b)) ^ (b' ^ a)) v ((a' ^ b') ^ (b' ^ a))) = ((((a ^ b) v (a' ^ b)) ^ (b' ^ a)) v 0)
130 or0 102 . . . . . . . . . . 11 ((((a ^ b) v (a' ^ b)) ^ (b' ^ a)) v 0) = (((a ^ b) v (a' ^ b)) ^ (b' ^ a))
131129, 130ax-r2 36 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b)) ^ (b' ^ a)) v ((a' ^ b') ^ (b' ^ a))) = (((a ^ b) v (a' ^ b)) ^ (b' ^ a))
132112, 131ax-r2 36 . . . . . . . . 9 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a)) = (((a ^ b) v (a' ^ b)) ^ (b' ^ a))
133105, 1322or 72 . . . . . . . 8 (((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b ^ a)) v ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a))) = ((((a ^ b) v (a' ^ b)) ^ (b ^ a)) v (((a ^ b) v (a' ^ b)) ^ (b' ^ a)))
1347, 8com2an 484 . . . . . . . . . . . . 13 (a ^ b) C (b' ^ a)
135134comcom 453 . . . . . . . . . . . 12 (b' ^ a) C (a ^ b)
136135, 109fh1r 473 . . . . . . . . . . 11 (((a ^ b) v (a' ^ b)) ^ (b' ^ a)) = (((a ^ b) ^ (b' ^ a)) v ((a' ^ b) ^ (b' ^ a)))
137 anass 76 . . . . . . . . . . . . . 14 ((a ^ b) ^ (b' ^ a)) = (a ^ (b ^ (b' ^ a)))
13897lan 77 . . . . . . . . . . . . . . 15 (a ^ (b ^ (b' ^ a))) = (a ^ 0)
139138, 56ax-r2 36 . . . . . . . . . . . . . 14 (a ^ (b ^ (b' ^ a))) = 0
140137, 139ax-r2 36 . . . . . . . . . . . . 13 ((a ^ b) ^ (b' ^ a)) = 0
141 anass 76 . . . . . . . . . . . . . 14 ((a' ^ b) ^ (b' ^ a)) = (a' ^ (b ^ (b' ^ a)))
14297lan 77 . . . . . . . . . . . . . . 15 (a' ^ (b ^ (b' ^ a))) = (a' ^ 0)
143142, 52ax-r2 36 . . . . . . . . . . . . . 14 (a' ^ (b ^ (b' ^ a))) = 0
144141, 143ax-r2 36 . . . . . . . . . . . . 13 ((a' ^ b) ^ (b' ^ a)) = 0
145140, 1442or 72 . . . . . . . . . . . 12 (((a ^ b) ^ (b' ^ a)) v ((a' ^ b) ^ (b' ^ a))) = (0 v 0)
146145, 67ax-r2 36 . . . . . . . . . . 11 (((a ^ b) ^ (b' ^ a)) v ((a' ^ b) ^ (b' ^ a))) = 0
147136, 146ax-r2 36 . . . . . . . . . 10 (((a ^ b) v (a' ^ b)) ^ (b' ^ a)) = 0
148147lor 70 . . . . . . . . 9 ((((a ^ b) v (a' ^ b)) ^ (b ^ a)) v (((a ^ b) v (a' ^ b)) ^ (b' ^ a))) = ((((a ^ b) v (a' ^ b)) ^ (b ^ a)) v 0)
14980, 81fh1r 473 . . . . . . . . . . 11 (((a ^ b) v (a' ^ b)) ^ (b ^ a)) = (((a ^ b) ^ (b ^ a)) v ((a' ^ b) ^ (b ^ a)))
150 ancom 74 . . . . . . . . . . . . . . 15 (b ^ a) = (a ^ b)
151150lan 77 . . . . . . . . . . . . . 14 ((a ^ b) ^ (b ^ a)) = ((a ^ b) ^ (a ^ b))
152 anidm 111 . . . . . . . . . . . . . 14 ((a ^ b) ^ (a ^ b)) = (a ^ b)
153151, 152ax-r2 36 . . . . . . . . . . . . 13 ((a ^ b) ^ (b ^ a)) = (a ^ b)
154 ancom 74 . . . . . . . . . . . . . 14 ((a' ^ b) ^ (b ^ a)) = ((b ^ a) ^ (a' ^ b))
155 anass 76 . . . . . . . . . . . . . . 15 ((b ^ a) ^ (a' ^ b)) = (b ^ (a ^ (a' ^ b)))
156 anass 76 . . . . . . . . . . . . . . . . . . . 20 ((a ^ a') ^ b) = (a ^ (a' ^ b))
157156ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (a ^ (a' ^ b)) = ((a ^ a') ^ b)
158119ran 78 . . . . . . . . . . . . . . . . . . . 20 ((a ^ a') ^ b) = (0 ^ b)
159 ancom 74 . . . . . . . . . . . . . . . . . . . 20 (0 ^ b) = (b ^ 0)
160158, 159ax-r2 36 . . . . . . . . . . . . . . . . . . 19 ((a ^ a') ^ b) = (b ^ 0)
161157, 160ax-r2 36 . . . . . . . . . . . . . . . . . 18 (a ^ (a' ^ b)) = (b ^ 0)
162 an0 108 . . . . . . . . . . . . . . . . . 18 (b ^ 0) = 0
163161, 162ax-r2 36 . . . . . . . . . . . . . . . . 17 (a ^ (a' ^ b)) = 0
164163lan 77 . . . . . . . . . . . . . . . 16 (b ^ (a ^ (a' ^ b))) = (b ^ 0)
165164, 162ax-r2 36 . . . . . . . . . . . . . . 15 (b ^ (a ^ (a' ^ b))) = 0
166155, 165ax-r2 36 . . . . . . . . . . . . . 14 ((b ^ a) ^ (a' ^ b)) = 0
167154, 166ax-r2 36 . . . . . . . . . . . . 13 ((a' ^ b) ^ (b ^ a)) = 0
168153, 1672or 72 . . . . . . . . . . . 12 (((a ^ b) ^ (b ^ a)) v ((a' ^ b) ^ (b ^ a))) = ((a ^ b) v 0)
169 or0 102 . . . . . . . . . . . 12 ((a ^ b) v 0) = (a ^ b)
170168, 169ax-r2 36 . . . . . . . . . . 11 (((a ^ b) ^ (b ^ a)) v ((a' ^ b) ^ (b ^ a))) = (a ^ b)
171149, 170ax-r2 36 . . . . . . . . . 10 (((a ^ b) v (a' ^ b)) ^ (b ^ a)) = (a ^ b)
172103, 171ax-r2 36 . . . . . . . . 9 ((((a ^ b) v (a' ^ b)) ^ (b ^ a)) v 0) = (a ^ b)
173148, 172ax-r2 36 . . . . . . . 8 ((((a ^ b) v (a' ^ b)) ^ (b ^ a)) v (((a ^ b) v (a' ^ b)) ^ (b' ^ a))) = (a ^ b)
174133, 173ax-r2 36 . . . . . . 7 (((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b ^ a)) v ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a))) = (a ^ b)
17586, 174ax-r2 36 . . . . . 6 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b ^ a) v (b' ^ a))) = (a ^ b)
17679, 1752or 72 . . . . 5 (((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a')) v ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b ^ a) v (b' ^ a)))) = ((a' ^ b') v (a ^ b))
177 ax-a2 31 . . . . 5 ((a' ^ b') v (a ^ b)) = ((a ^ b) v (a' ^ b'))
178176, 177ax-r2 36 . . . 4 (((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a')) v ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b ^ a) v (b' ^ a)))) = ((a ^ b) v (a' ^ b'))
17934, 178ax-r2 36 . . 3 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b' ^ a') v ((b ^ a) v (b' ^ a)))) = ((a ^ b) v (a' ^ b'))
1805, 179ax-r2 36 . 2 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (((b ^ a) v (b' ^ a)) v (b' ^ a'))) = ((a ^ b) v (a' ^ b'))
1813, 180ax-r2 36 1 ((a ->5 b) ^ (b ->5 a)) = ((a ^ b) v (a' ^ b'))
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  0wf 9   ->5 wi5 16
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-i5 48  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud5lem1  589
  Copyright terms: Public domain W3C validator