QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud3lem3 Unicode version
Theorem ud3lem3 576
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud3lem3 ((a ->3 b) ->3 (a v b)) = (a v b)
Proof of Theorem ud3lem3
StepHypRef Expression
1 df-i3 46 . 2 ((a ->3 b) ->3 (a v b)) = ((((a ->3 b)' ^ (a v b)) v ((a ->3 b)' ^ (a v b)')) v ((a ->3 b) ^ ((a ->3 b)' v (a v b))))
2 ud3lem3a 572 . . . . . . 7 ((a ->3 b)' ^ (a v b)) = (a ->3 b)'
3 ud3lem0c 279 . . . . . . 7 (a ->3 b)' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
42, 3ax-r2 36 . . . . . 6 ((a ->3 b)' ^ (a v b)) = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
5 ud3lem3b 573 . . . . . 6 ((a ->3 b)' ^ (a v b)') = 0
64, 52or 72 . . . . 5 (((a ->3 b)' ^ (a v b)) v ((a ->3 b)' ^ (a v b)')) = ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v 0)
7 or0 102 . . . . 5 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v 0) = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
86, 7ax-r2 36 . . . 4 (((a ->3 b)' ^ (a v b)) v ((a ->3 b)' ^ (a v b)')) = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
9 ud3lem3d 575 . . . 4 ((a ->3 b) ^ ((a ->3 b)' v (a v b))) = ((a' ^ b) v (a ^ (a' v b)))
108, 92or 72 . . 3 ((((a ->3 b)' ^ (a v b)) v ((a ->3 b)' ^ (a v b)')) v ((a ->3 b) ^ ((a ->3 b)' v (a v b)))) = ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v ((a' ^ b) v (a ^ (a' v b))))
11 coman1 185 . . . . . . . . . 10 (a' ^ b) C a'
1211comcom7 460 . . . . . . . . 9 (a' ^ b) C a
13 coman2 186 . . . . . . . . . 10 (a' ^ b) C b
1413comcom2 183 . . . . . . . . 9 (a' ^ b) C b'
1512, 14com2or 483 . . . . . . . 8 (a' ^ b) C (a v b')
1612, 13com2or 483 . . . . . . . 8 (a' ^ b) C (a v b)
1715, 16com2an 484 . . . . . . 7 (a' ^ b) C ((a v b') ^ (a v b))
1817comcom 453 . . . . . 6 ((a v b') ^ (a v b)) C (a' ^ b)
19 comorr 184 . . . . . . . . 9 a C (a v b')
20 comorr 184 . . . . . . . . 9 a C (a v b)
2119, 20com2an 484 . . . . . . . 8 a C ((a v b') ^ (a v b))
2221comcom 453 . . . . . . 7 ((a v b') ^ (a v b)) C a
23 comor1 461 . . . . . . . . . . 11 (a' v b) C a'
2423comcom7 460 . . . . . . . . . 10 (a' v b) C a
25 comor2 462 . . . . . . . . . . 11 (a' v b) C b
2625comcom2 183 . . . . . . . . . 10 (a' v b) C b'
2724, 26com2or 483 . . . . . . . . 9 (a' v b) C (a v b')
2824, 25com2or 483 . . . . . . . . 9 (a' v b) C (a v b)
2927, 28com2an 484 . . . . . . . 8 (a' v b) C ((a v b') ^ (a v b))
3029comcom 453 . . . . . . 7 ((a v b') ^ (a v b)) C (a' v b)
3122, 30com2an 484 . . . . . 6 ((a v b') ^ (a v b)) C (a ^ (a' v b))
3218, 31com2or 483 . . . . 5 ((a v b') ^ (a v b)) C ((a' ^ b) v (a ^ (a' v b)))
3319comcom3 454 . . . . . . . 8 a' C (a v b')
3420comcom3 454 . . . . . . . 8 a' C (a v b)
3533, 34com2an 484 . . . . . . 7 a' C ((a v b') ^ (a v b))
3635comcom 453 . . . . . 6 ((a v b') ^ (a v b)) C a'
37 coman1 185 . . . . . . . . 9 (a ^ b') C a
38 coman2 186 . . . . . . . . 9 (a ^ b') C b'
3937, 38com2or 483 . . . . . . . 8 (a ^ b') C (a v b')
4038comcom7 460 . . . . . . . . 9 (a ^ b') C b
4137, 40com2or 483 . . . . . . . 8 (a ^ b') C (a v b)
4239, 41com2an 484 . . . . . . 7 (a ^ b') C ((a v b') ^ (a v b))
4342comcom 453 . . . . . 6 ((a v b') ^ (a v b)) C (a ^ b')
4436, 43com2or 483 . . . . 5 ((a v b') ^ (a v b)) C (a' v (a ^ b'))
4532, 44fh4r 476 . . . 4 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v ((a' ^ b) v (a ^ (a' v b)))) = ((((a v b') ^ (a v b)) v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a' v (a ^ b')) v ((a' ^ b) v (a ^ (a' v b)))))
46 comor1 461 . . . . . . . . . . 11 (a v b') C a
4746comcom2 183 . . . . . . . . . 10 (a v b') C a'
48 comor2 462 . . . . . . . . . . 11 (a v b') C b'
4948comcom7 460 . . . . . . . . . 10 (a v b') C b
5047, 49com2an 484 . . . . . . . . 9 (a v b') C (a' ^ b)
5147, 49com2or 483 . . . . . . . . . 10 (a v b') C (a' v b)
5246, 51com2an 484 . . . . . . . . 9 (a v b') C (a ^ (a' v b))
5350, 52com2or 483 . . . . . . . 8 (a v b') C ((a' ^ b) v (a ^ (a' v b)))
5446, 49com2or 483 . . . . . . . 8 (a v b') C (a v b)
5553, 54fh4r 476 . . . . . . 7 (((a v b') ^ (a v b)) v ((a' ^ b) v (a ^ (a' v b)))) = (((a v b') v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a v b) v ((a' ^ b) v (a ^ (a' v b)))))
56 ax-a3 32 . . . . . . . . . . 11 (((a v b') v (a' ^ b)) v (a ^ (a' v b))) = ((a v b') v ((a' ^ b) v (a ^ (a' v b))))
5756ax-r1 35 . . . . . . . . . 10 ((a v b') v ((a' ^ b) v (a ^ (a' v b)))) = (((a v b') v (a' ^ b)) v (a ^ (a' v b)))
58 anor2 89 . . . . . . . . . . . . . 14 (a' ^ b) = (a v b')'
5958lor 70 . . . . . . . . . . . . 13 ((a v b') v (a' ^ b)) = ((a v b') v (a v b')')
60 df-t 41 . . . . . . . . . . . . . 14 1 = ((a v b') v (a v b')')
6160ax-r1 35 . . . . . . . . . . . . 13 ((a v b') v (a v b')') = 1
6259, 61ax-r2 36 . . . . . . . . . . . 12 ((a v b') v (a' ^ b)) = 1
6362ax-r5 38 . . . . . . . . . . 11 (((a v b') v (a' ^ b)) v (a ^ (a' v b))) = (1 v (a ^ (a' v b)))
64 or1r 105 . . . . . . . . . . 11 (1 v (a ^ (a' v b))) = 1
6563, 64ax-r2 36 . . . . . . . . . 10 (((a v b') v (a' ^ b)) v (a ^ (a' v b))) = 1
6657, 65ax-r2 36 . . . . . . . . 9 ((a v b') v ((a' ^ b) v (a ^ (a' v b)))) = 1
67 ax-a2 31 . . . . . . . . . 10 ((a v b) v ((a' ^ b) v (a ^ (a' v b)))) = (((a' ^ b) v (a ^ (a' v b))) v (a v b))
68 lear 161 . . . . . . . . . . . . 13 (a' ^ b) =< b
69 leor 159 . . . . . . . . . . . . 13 b =< (a v b)
7068, 69letr 137 . . . . . . . . . . . 12 (a' ^ b) =< (a v b)
71 lea 160 . . . . . . . . . . . . 13 (a ^ (a' v b)) =< a
72 leo 158 . . . . . . . . . . . . 13 a =< (a v b)
7371, 72letr 137 . . . . . . . . . . . 12 (a ^ (a' v b)) =< (a v b)
7470, 73lel2or 170 . . . . . . . . . . 11 ((a' ^ b) v (a ^ (a' v b))) =< (a v b)
7574df-le2 131 . . . . . . . . . 10 (((a' ^ b) v (a ^ (a' v b))) v (a v b)) = (a v b)
7667, 75ax-r2 36 . . . . . . . . 9 ((a v b) v ((a' ^ b) v (a ^ (a' v b)))) = (a v b)
7766, 762an 79 . . . . . . . 8 (((a v b') v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a v b) v ((a' ^ b) v (a ^ (a' v b))))) = (1 ^ (a v b))
78 an1r 107 . . . . . . . 8 (1 ^ (a v b)) = (a v b)
7977, 78ax-r2 36 . . . . . . 7 (((a v b') v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a v b) v ((a' ^ b) v (a ^ (a' v b))))) = (a v b)
8055, 79ax-r2 36 . . . . . 6 (((a v b') ^ (a v b)) v ((a' ^ b) v (a ^ (a' v b)))) = (a v b)
81 or12 80 . . . . . . 7 ((a' v (a ^ b')) v ((a' ^ b) v (a ^ (a' v b)))) = ((a' ^ b) v ((a' v (a ^ b')) v (a ^ (a' v b))))
82 df-a 40 . . . . . . . . . . . 12 (a ^ (a' v b)) = (a' v (a' v b)')'
83 anor1 88 . . . . . . . . . . . . . . 15 (a ^ b') = (a' v b)'
8483ax-r1 35 . . . . . . . . . . . . . 14 (a' v b)' = (a ^ b')
8584lor 70 . . . . . . . . . . . . 13 (a' v (a' v b)') = (a' v (a ^ b'))
8685ax-r4 37 . . . . . . . . . . . 12 (a' v (a' v b)')' = (a' v (a ^ b'))'
8782, 86ax-r2 36 . . . . . . . . . . 11 (a ^ (a' v b)) = (a' v (a ^ b'))'
8887lor 70 . . . . . . . . . 10 ((a' v (a ^ b')) v (a ^ (a' v b))) = ((a' v (a ^ b')) v (a' v (a ^ b'))')
89 df-t 41 . . . . . . . . . . 11 1 = ((a' v (a ^ b')) v (a' v (a ^ b'))')
9089ax-r1 35 . . . . . . . . . 10 ((a' v (a ^ b')) v (a' v (a ^ b'))') = 1
9188, 90ax-r2 36 . . . . . . . . 9 ((a' v (a ^ b')) v (a ^ (a' v b))) = 1
9291lor 70 . . . . . . . 8 ((a' ^ b) v ((a' v (a ^ b')) v (a ^ (a' v b)))) = ((a' ^ b) v 1)
93 or1 104 . . . . . . . 8 ((a' ^ b) v 1) = 1
9492, 93ax-r2 36 . . . . . . 7 ((a' ^ b) v ((a' v (a ^ b')) v (a ^ (a' v b)))) = 1
9581, 94ax-r2 36 . . . . . 6 ((a' v (a ^ b')) v ((a' ^ b) v (a ^ (a' v b)))) = 1
9680, 952an 79 . . . . 5 ((((a v b') ^ (a v b)) v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a' v (a ^ b')) v ((a' ^ b) v (a ^ (a' v b))))) = ((a v b) ^ 1)
97 an1 106 . . . . 5 ((a v b) ^ 1) = (a v b)
9896, 97ax-r2 36 . . . 4 ((((a v b') ^ (a v b)) v ((a' ^ b) v (a ^ (a' v b)))) ^ ((a' v (a ^ b')) v ((a' ^ b) v (a ^ (a' v b))))) = (a v b)
9945, 98ax-r2 36 . . 3 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) v ((a' ^ b) v (a ^ (a' v b)))) = (a v b)
10010, 99ax-r2 36 . 2 ((((a ->3 b)' ^ (a v b)) v ((a ->3 b)' ^ (a v b)')) v ((a ->3 b) ^ ((a ->3 b)' v (a v b)))) = (a v b)
1011, 100ax-r2 36 1 ((a ->3 b) ->3 (a v b)) = (a v b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8  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:  ud3  597
  Copyright terms: Public domain W3C validator