QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud1lem3 Unicode version
Theorem ud1lem3 562
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud1lem3 ((a ->1 b) ->1 (a v b)) = (a v b)
Proof of Theorem ud1lem3
StepHypRef Expression
1 df-i1 44 . 2 ((a ->1 b) ->1 (a v b)) = ((a ->1 b)' v ((a ->1 b) ^ (a v b)))
2 ud1lem0c 277 . . . 4 (a ->1 b)' = (a ^ (a' v b'))
32con3 68 . . . . 5 (a ->1 b) = (a ^ (a' v b'))'
43ran 78 . . . 4 ((a ->1 b) ^ (a v b)) = ((a ^ (a' v b'))' ^ (a v b))
52, 42or 72 . . 3 ((a ->1 b)' v ((a ->1 b) ^ (a v b))) = ((a ^ (a' v b')) v ((a ^ (a' v b'))' ^ (a v b)))
6 comid 187 . . . . . 6 (a ^ (a' v b')) C (a ^ (a' v b'))
76comcom2 183 . . . . 5 (a ^ (a' v b')) C (a ^ (a' v b'))'
8 comor1 461 . . . . . . 7 (a v b) C a
98comcom2 183 . . . . . . . 8 (a v b) C a'
10 comor2 462 . . . . . . . . 9 (a v b) C b
1110comcom2 183 . . . . . . . 8 (a v b) C b'
129, 11com2or 483 . . . . . . 7 (a v b) C (a' v b')
138, 12com2an 484 . . . . . 6 (a v b) C (a ^ (a' v b'))
1413comcom 453 . . . . 5 (a ^ (a' v b')) C (a v b)
157, 14fh3 471 . . . 4 ((a ^ (a' v b')) v ((a ^ (a' v b'))' ^ (a v b))) = (((a ^ (a' v b')) v (a ^ (a' v b'))') ^ ((a ^ (a' v b')) v (a v b)))
16 ancom 74 . . . . 5 (((a ^ (a' v b')) v (a ^ (a' v b'))') ^ ((a ^ (a' v b')) v (a v b))) = (((a ^ (a' v b')) v (a v b)) ^ ((a ^ (a' v b')) v (a ^ (a' v b'))'))
17 df-t 41 . . . . . . . 8 1 = ((a ^ (a' v b')) v (a ^ (a' v b'))')
1817ax-r1 35 . . . . . . 7 ((a ^ (a' v b')) v (a ^ (a' v b'))') = 1
1918lan 77 . . . . . 6 (((a ^ (a' v b')) v (a v b)) ^ ((a ^ (a' v b')) v (a ^ (a' v b'))')) = (((a ^ (a' v b')) v (a v b)) ^ 1)
20 an1 106 . . . . . . 7 (((a ^ (a' v b')) v (a v b)) ^ 1) = ((a ^ (a' v b')) v (a v b))
21 comorr 184 . . . . . . . . 9 a C (a v b)
22 comorr 184 . . . . . . . . . . 11 a' C (a' v b')
2322comcom2 183 . . . . . . . . . 10 a' C (a' v b')'
2423comcom5 458 . . . . . . . . 9 a C (a' v b')
2521, 24fh4r 476 . . . . . . . 8 ((a ^ (a' v b')) v (a v b)) = ((a v (a v b)) ^ ((a' v b') v (a v b)))
26 ax-a2 31 . . . . . . . . . . 11 ((a' v b') v (a v b)) = ((a v b) v (a' v b'))
27 or4 84 . . . . . . . . . . . 12 ((a v b) v (a' v b')) = ((a v a') v (b v b'))
28 df-t 41 . . . . . . . . . . . . . . 15 1 = (b v b')
2928ax-r1 35 . . . . . . . . . . . . . 14 (b v b') = 1
3029lor 70 . . . . . . . . . . . . 13 ((a v a') v (b v b')) = ((a v a') v 1)
31 or1 104 . . . . . . . . . . . . 13 ((a v a') v 1) = 1
3230, 31ax-r2 36 . . . . . . . . . . . 12 ((a v a') v (b v b')) = 1
3327, 32ax-r2 36 . . . . . . . . . . 11 ((a v b) v (a' v b')) = 1
3426, 33ax-r2 36 . . . . . . . . . 10 ((a' v b') v (a v b)) = 1
3534lan 77 . . . . . . . . 9 ((a v (a v b)) ^ ((a' v b') v (a v b))) = ((a v (a v b)) ^ 1)
36 an1 106 . . . . . . . . . 10 ((a v (a v b)) ^ 1) = (a v (a v b))
37 ax-a3 32 . . . . . . . . . . . 12 ((a v a) v b) = (a v (a v b))
3837ax-r1 35 . . . . . . . . . . 11 (a v (a v b)) = ((a v a) v b)
39 oridm 110 . . . . . . . . . . . 12 (a v a) = a
4039ax-r5 38 . . . . . . . . . . 11 ((a v a) v b) = (a v b)
4138, 40ax-r2 36 . . . . . . . . . 10 (a v (a v b)) = (a v b)
4236, 41ax-r2 36 . . . . . . . . 9 ((a v (a v b)) ^ 1) = (a v b)
4335, 42ax-r2 36 . . . . . . . 8 ((a v (a v b)) ^ ((a' v b') v (a v b))) = (a v b)
4425, 43ax-r2 36 . . . . . . 7 ((a ^ (a' v b')) v (a v b)) = (a v b)
4520, 44ax-r2 36 . . . . . 6 (((a ^ (a' v b')) v (a v b)) ^ 1) = (a v b)
4619, 45ax-r2 36 . . . . 5 (((a ^ (a' v b')) v (a v b)) ^ ((a ^ (a' v b')) v (a ^ (a' v b'))')) = (a v b)
4716, 46ax-r2 36 . . . 4 (((a ^ (a' v b')) v (a ^ (a' v b'))') ^ ((a ^ (a' v b')) v (a v b))) = (a v b)
4815, 47ax-r2 36 . . 3 ((a ^ (a' v b')) v ((a ^ (a' v b'))' ^ (a v b))) = (a v b)
495, 48ax-r2 36 . 2 ((a ->1 b)' v ((a ->1 b) ^ (a v b))) = (a v b)
501, 49ax-r2 36 1 ((a ->1 b) ->1 (a v b)) = (a v b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8   ->1 wi1 12
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-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud1  595
  Copyright terms: Public domain W3C validator