QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud4lem2 Unicode version
Theorem ud4lem2 582
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud4lem2 ((a v (a' ^ b')) ->4 a) = (a v b)
Proof of Theorem ud4lem2
StepHypRef Expression
1 df-i4 47 . 2 ((a v (a' ^ b')) ->4 a) = ((((a v (a' ^ b')) ^ a) v ((a v (a' ^ b'))' ^ a)) v (((a v (a' ^ b'))' v a) ^ a'))
2 ancom 74 . . . . . . 7 ((a v (a' ^ b')) ^ a) = (a ^ (a v (a' ^ b')))
3 anabs 121 . . . . . . 7 (a ^ (a v (a' ^ b'))) = a
42, 3ax-r2 36 . . . . . 6 ((a v (a' ^ b')) ^ a) = a
5 oran 87 . . . . . . . . 9 (a v (a' ^ b')) = (a' ^ (a' ^ b')')'
65con2 67 . . . . . . . 8 (a v (a' ^ b'))' = (a' ^ (a' ^ b')')
76ran 78 . . . . . . 7 ((a v (a' ^ b'))' ^ a) = ((a' ^ (a' ^ b')') ^ a)
8 ancom 74 . . . . . . . 8 ((a' ^ (a' ^ b')') ^ a) = (a ^ (a' ^ (a' ^ b')'))
9 anass 76 . . . . . . . . . 10 ((a ^ a') ^ (a' ^ b')') = (a ^ (a' ^ (a' ^ b')'))
109ax-r1 35 . . . . . . . . 9 (a ^ (a' ^ (a' ^ b')')) = ((a ^ a') ^ (a' ^ b')')
11 ancom 74 . . . . . . . . . 10 ((a ^ a') ^ (a' ^ b')') = ((a' ^ b')' ^ (a ^ a'))
12 dff 101 . . . . . . . . . . . . 13 0 = (a ^ a')
1312lan 77 . . . . . . . . . . . 12 ((a' ^ b')' ^ 0) = ((a' ^ b')' ^ (a ^ a'))
1413ax-r1 35 . . . . . . . . . . 11 ((a' ^ b')' ^ (a ^ a')) = ((a' ^ b')' ^ 0)
15 an0 108 . . . . . . . . . . 11 ((a' ^ b')' ^ 0) = 0
1614, 15ax-r2 36 . . . . . . . . . 10 ((a' ^ b')' ^ (a ^ a')) = 0
1711, 16ax-r2 36 . . . . . . . . 9 ((a ^ a') ^ (a' ^ b')') = 0
1810, 17ax-r2 36 . . . . . . . 8 (a ^ (a' ^ (a' ^ b')')) = 0
198, 18ax-r2 36 . . . . . . 7 ((a' ^ (a' ^ b')') ^ a) = 0
207, 19ax-r2 36 . . . . . 6 ((a v (a' ^ b'))' ^ a) = 0
214, 202or 72 . . . . 5 (((a v (a' ^ b')) ^ a) v ((a v (a' ^ b'))' ^ a)) = (a v 0)
22 or0 102 . . . . 5 (a v 0) = a
2321, 22ax-r2 36 . . . 4 (((a v (a' ^ b')) ^ a) v ((a v (a' ^ b'))' ^ a)) = a
24 ancom 74 . . . . 5 (((a v (a' ^ b'))' v a) ^ a') = (a' ^ ((a v (a' ^ b'))' v a))
25 oran 87 . . . . . . . . . . . . 13 (a v b) = (a' ^ b')'
2625ax-r1 35 . . . . . . . . . . . 12 (a' ^ b')' = (a v b)
2726con3 68 . . . . . . . . . . 11 (a' ^ b') = (a v b)'
2827lor 70 . . . . . . . . . 10 (a v (a' ^ b')) = (a v (a v b)')
29 anor2 89 . . . . . . . . . . . 12 (a' ^ (a v b)) = (a v (a v b)')'
3029ax-r1 35 . . . . . . . . . . 11 (a v (a v b)')' = (a' ^ (a v b))
3130con3 68 . . . . . . . . . 10 (a v (a v b)') = (a' ^ (a v b))'
3228, 31ax-r2 36 . . . . . . . . 9 (a v (a' ^ b')) = (a' ^ (a v b))'
3332con2 67 . . . . . . . 8 (a v (a' ^ b'))' = (a' ^ (a v b))
3433ax-r5 38 . . . . . . 7 ((a v (a' ^ b'))' v a) = ((a' ^ (a v b)) v a)
35 comid 187 . . . . . . . . . 10 a C a
3635comcom2 183 . . . . . . . . 9 a C a'
37 comorr 184 . . . . . . . . 9 a C (a v b)
3836, 37fh3r 475 . . . . . . . 8 ((a' ^ (a v b)) v a) = ((a' v a) ^ ((a v b) v a))
39 ancom 74 . . . . . . . . . 10 ((a' v a) ^ ((a v b) v a)) = (((a v b) v a) ^ (a' v a))
40 or32 82 . . . . . . . . . . . 12 ((a v b) v a) = ((a v a) v b)
41 oridm 110 . . . . . . . . . . . . 13 (a v a) = a
4241ax-r5 38 . . . . . . . . . . . 12 ((a v a) v b) = (a v b)
4340, 42ax-r2 36 . . . . . . . . . . 11 ((a v b) v a) = (a v b)
44 df-t 41 . . . . . . . . . . . . 13 1 = (a v a')
45 ax-a2 31 . . . . . . . . . . . . 13 (a v a') = (a' v a)
4644, 45ax-r2 36 . . . . . . . . . . . 12 1 = (a' v a)
4746ax-r1 35 . . . . . . . . . . 11 (a' v a) = 1
4843, 472an 79 . . . . . . . . . 10 (((a v b) v a) ^ (a' v a)) = ((a v b) ^ 1)
4939, 48ax-r2 36 . . . . . . . . 9 ((a' v a) ^ ((a v b) v a)) = ((a v b) ^ 1)
50 an1 106 . . . . . . . . 9 ((a v b) ^ 1) = (a v b)
5149, 50ax-r2 36 . . . . . . . 8 ((a' v a) ^ ((a v b) v a)) = (a v b)
5238, 51ax-r2 36 . . . . . . 7 ((a' ^ (a v b)) v a) = (a v b)
5334, 52ax-r2 36 . . . . . 6 ((a v (a' ^ b'))' v a) = (a v b)
5453lan 77 . . . . 5 (a' ^ ((a v (a' ^ b'))' v a)) = (a' ^ (a v b))
5524, 54ax-r2 36 . . . 4 (((a v (a' ^ b'))' v a) ^ a') = (a' ^ (a v b))
5623, 552or 72 . . 3 ((((a v (a' ^ b')) ^ a) v ((a v (a' ^ b'))' ^ a)) v (((a v (a' ^ b'))' v a) ^ a')) = (a v (a' ^ (a v b)))
57 oml 445 . . 3 (a v (a' ^ (a v b))) = (a v b)
5856, 57ax-r2 36 . 2 ((((a v (a' ^ b')) ^ a) v ((a v (a' ^ b'))' ^ a)) v (((a v (a' ^ b'))' v a) ^ a')) = (a v b)
591, 58ax-r2 36 1 ((a v (a' ^ b')) ->4 a) = (a v b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8  0wf 9   ->4 wi4 15
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-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud4  598
  Copyright terms: Public domain W3C validator