QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud5lem3 Unicode version
Theorem ud5lem3 594
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud5lem3 ((a ->5 b) ->5 (a v (a' ^ b))) = (a v b)
Proof of Theorem ud5lem3
StepHypRef Expression
1 df-i5 48 . 2 ((a ->5 b) ->5 (a v (a' ^ b))) = ((((a ->5 b) ^ (a v (a' ^ b))) v ((a ->5 b)' ^ (a v (a' ^ b)))) v ((a ->5 b)' ^ (a v (a' ^ b))'))
2 ud5lem3a 591 . . . . 5 ((a ->5 b) ^ (a v (a' ^ b))) = ((a ^ b) v (a' ^ b))
3 ud5lem3b 592 . . . . 5 ((a ->5 b)' ^ (a v (a' ^ b))) = (a ^ (a' v b'))
42, 32or 72 . . . 4 (((a ->5 b) ^ (a v (a' ^ b))) v ((a ->5 b)' ^ (a v (a' ^ b)))) = (((a ^ b) v (a' ^ b)) v (a ^ (a' v b')))
5 ud5lem3c 593 . . . 4 ((a ->5 b)' ^ (a v (a' ^ b))') = (((a v b) ^ (a v b')) ^ a')
64, 52or 72 . . 3 ((((a ->5 b) ^ (a v (a' ^ b))) v ((a ->5 b)' ^ (a v (a' ^ b)))) v ((a ->5 b)' ^ (a v (a' ^ b))')) = ((((a ^ b) v (a' ^ b)) v (a ^ (a' v b'))) v (((a v b) ^ (a v b')) ^ a'))
7 ax-a3 32 . . . 4 ((((a ^ b) v (a' ^ b)) v (a ^ (a' v b'))) v (((a v b) ^ (a v b')) ^ a')) = (((a ^ b) v (a' ^ b)) v ((a ^ (a' v b')) v (((a v b) ^ (a v b')) ^ a')))
8 or4 84 . . . . 5 (((a ^ b) v (a' ^ b)) v ((a ^ (a' v b')) v (((a v b) ^ (a v b')) ^ a'))) = (((a ^ b) v (a ^ (a' v b'))) v ((a' ^ b) v (((a v b) ^ (a v b')) ^ a')))
9 comanr1 464 . . . . . . . . 9 a C (a ^ b)
10 comorr 184 . . . . . . . . . 10 a' C (a' v b')
1110comcom6 459 . . . . . . . . 9 a C (a' v b')
129, 11fh4 472 . . . . . . . 8 ((a ^ b) v (a ^ (a' v b'))) = (((a ^ b) v a) ^ ((a ^ b) v (a' v b')))
13 ax-a2 31 . . . . . . . . . . 11 ((a ^ b) v a) = (a v (a ^ b))
14 orabs 120 . . . . . . . . . . 11 (a v (a ^ b)) = a
1513, 14ax-r2 36 . . . . . . . . . 10 ((a ^ b) v a) = a
16 df-a 40 . . . . . . . . . . . . . 14 (a ^ b) = (a' v b')'
1716ax-r1 35 . . . . . . . . . . . . 13 (a' v b')' = (a ^ b)
1817con3 68 . . . . . . . . . . . 12 (a' v b') = (a ^ b)'
1918lor 70 . . . . . . . . . . 11 ((a ^ b) v (a' v b')) = ((a ^ b) v (a ^ b)')
20 df-t 41 . . . . . . . . . . . 12 1 = ((a ^ b) v (a ^ b)')
2120ax-r1 35 . . . . . . . . . . 11 ((a ^ b) v (a ^ b)') = 1
2219, 21ax-r2 36 . . . . . . . . . 10 ((a ^ b) v (a' v b')) = 1
2315, 222an 79 . . . . . . . . 9 (((a ^ b) v a) ^ ((a ^ b) v (a' v b'))) = (a ^ 1)
24 an1 106 . . . . . . . . 9 (a ^ 1) = a
2523, 24ax-r2 36 . . . . . . . 8 (((a ^ b) v a) ^ ((a ^ b) v (a' v b'))) = a
2612, 25ax-r2 36 . . . . . . 7 ((a ^ b) v (a ^ (a' v b'))) = a
27 coman1 185 . . . . . . . . . . . 12 (a' ^ b) C a'
2827comcom7 460 . . . . . . . . . . 11 (a' ^ b) C a
29 coman2 186 . . . . . . . . . . 11 (a' ^ b) C b
3028, 29com2or 483 . . . . . . . . . 10 (a' ^ b) C (a v b)
3129comcom2 183 . . . . . . . . . . 11 (a' ^ b) C b'
3228, 31com2or 483 . . . . . . . . . 10 (a' ^ b) C (a v b')
3330, 32com2an 484 . . . . . . . . 9 (a' ^ b) C ((a v b) ^ (a v b'))
3433, 27fh3 471 . . . . . . . 8 ((a' ^ b) v (((a v b) ^ (a v b')) ^ a')) = (((a' ^ b) v ((a v b) ^ (a v b'))) ^ ((a' ^ b) v a'))
35 comor1 461 . . . . . . . . . . . . . 14 (a v b) C a
3635comcom2 183 . . . . . . . . . . . . 13 (a v b) C a'
37 comor2 462 . . . . . . . . . . . . 13 (a v b) C b
3836, 37com2an 484 . . . . . . . . . . . 12 (a v b) C (a' ^ b)
3937comcom2 183 . . . . . . . . . . . . 13 (a v b) C b'
4035, 39com2or 483 . . . . . . . . . . . 12 (a v b) C (a v b')
4138, 40fh4 472 . . . . . . . . . . 11 ((a' ^ b) v ((a v b) ^ (a v b'))) = (((a' ^ b) v (a v b)) ^ ((a' ^ b) v (a v b')))
4236, 37fh3r 475 . . . . . . . . . . . . . 14 ((a' ^ b) v (a v b)) = ((a' v (a v b)) ^ (b v (a v b)))
43 ax-a2 31 . . . . . . . . . . . . . . . 16 (a' v (a v b)) = ((a v b) v a')
44 or12 80 . . . . . . . . . . . . . . . . 17 (b v (a v b)) = (a v (b v b))
45 oridm 110 . . . . . . . . . . . . . . . . . 18 (b v b) = b
4645lor 70 . . . . . . . . . . . . . . . . 17 (a v (b v b)) = (a v b)
4744, 46ax-r2 36 . . . . . . . . . . . . . . . 16 (b v (a v b)) = (a v b)
4843, 472an 79 . . . . . . . . . . . . . . 15 ((a' v (a v b)) ^ (b v (a v b))) = (((a v b) v a') ^ (a v b))
49 ancom 74 . . . . . . . . . . . . . . . 16 (((a v b) v a') ^ (a v b)) = ((a v b) ^ ((a v b) v a'))
50 anabs 121 . . . . . . . . . . . . . . . 16 ((a v b) ^ ((a v b) v a')) = (a v b)
5149, 50ax-r2 36 . . . . . . . . . . . . . . 15 (((a v b) v a') ^ (a v b)) = (a v b)
5248, 51ax-r2 36 . . . . . . . . . . . . . 14 ((a' v (a v b)) ^ (b v (a v b))) = (a v b)
5342, 52ax-r2 36 . . . . . . . . . . . . 13 ((a' ^ b) v (a v b)) = (a v b)
54 anor2 89 . . . . . . . . . . . . . . . . 17 (a' ^ b) = (a v b')'
5554ax-r1 35 . . . . . . . . . . . . . . . 16 (a v b')' = (a' ^ b)
5655con3 68 . . . . . . . . . . . . . . 15 (a v b') = (a' ^ b)'
5756lor 70 . . . . . . . . . . . . . 14 ((a' ^ b) v (a v b')) = ((a' ^ b) v (a' ^ b)')
58 df-t 41 . . . . . . . . . . . . . . 15 1 = ((a' ^ b) v (a' ^ b)')
5958ax-r1 35 . . . . . . . . . . . . . 14 ((a' ^ b) v (a' ^ b)') = 1
6057, 59ax-r2 36 . . . . . . . . . . . . 13 ((a' ^ b) v (a v b')) = 1
6153, 602an 79 . . . . . . . . . . . 12 (((a' ^ b) v (a v b)) ^ ((a' ^ b) v (a v b'))) = ((a v b) ^ 1)
62 an1 106 . . . . . . . . . . . 12 ((a v b) ^ 1) = (a v b)
6361, 62ax-r2 36 . . . . . . . . . . 11 (((a' ^ b) v (a v b)) ^ ((a' ^ b) v (a v b'))) = (a v b)
6441, 63ax-r2 36 . . . . . . . . . 10 ((a' ^ b) v ((a v b) ^ (a v b'))) = (a v b)
65 ax-a2 31 . . . . . . . . . . 11 ((a' ^ b) v a') = (a' v (a' ^ b))
66 orabs 120 . . . . . . . . . . 11 (a' v (a' ^ b)) = a'
6765, 66ax-r2 36 . . . . . . . . . 10 ((a' ^ b) v a') = a'
6864, 672an 79 . . . . . . . . 9 (((a' ^ b) v ((a v b) ^ (a v b'))) ^ ((a' ^ b) v a')) = ((a v b) ^ a')
69 ancom 74 . . . . . . . . 9 ((a v b) ^ a') = (a' ^ (a v b))
7068, 69ax-r2 36 . . . . . . . 8 (((a' ^ b) v ((a v b) ^ (a v b'))) ^ ((a' ^ b) v a')) = (a' ^ (a v b))
7134, 70ax-r2 36 . . . . . . 7 ((a' ^ b) v (((a v b) ^ (a v b')) ^ a')) = (a' ^ (a v b))
7226, 712or 72 . . . . . 6 (((a ^ b) v (a ^ (a' v b'))) v ((a' ^ b) v (((a v b) ^ (a v b')) ^ a'))) = (a v (a' ^ (a v b)))
73 oml 445 . . . . . 6 (a v (a' ^ (a v b))) = (a v b)
7472, 73ax-r2 36 . . . . 5 (((a ^ b) v (a ^ (a' v b'))) v ((a' ^ b) v (((a v b) ^ (a v b')) ^ a'))) = (a v b)
758, 74ax-r2 36 . . . 4 (((a ^ b) v (a' ^ b)) v ((a ^ (a' v b')) v (((a v b) ^ (a v b')) ^ a'))) = (a v b)
767, 75ax-r2 36 . . 3 ((((a ^ b) v (a' ^ b)) v (a ^ (a' v b'))) v (((a v b) ^ (a v b')) ^ a')) = (a v b)
776, 76ax-r2 36 . 2 ((((a ->5 b) ^ (a v (a' ^ b))) v ((a ->5 b)' ^ (a v (a' ^ b)))) v ((a ->5 b)' ^ (a v (a' ^ b))')) = (a v b)
781, 77ax-r2 36 1 ((a ->5 b) ->5 (a v (a' ^ b))) = (a v b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8   ->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:  ud5  599
  Copyright terms: Public domain W3C validator