QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ni31 Unicode version
Theorem ni31 250
Description: Equivalence for Kalmbach implication.
Assertion
Ref Expression
ni31 (a ->3 b)' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
Proof of Theorem ni31
StepHypRef Expression
1 df-i3 46 . . 3 (a ->3 b) = (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))
2 oran 87 . . . 4 (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))) = (((a' ^ b) v (a' ^ b'))' ^ (a ^ (a' v b))')'
3 oran 87 . . . . . . . 8 ((a' ^ b) v (a' ^ b')) = ((a' ^ b)' ^ (a' ^ b')')'
4 anor2 89 . . . . . . . . . . 11 (a' ^ b) = (a v b')'
54con2 67 . . . . . . . . . 10 (a' ^ b)' = (a v b')
6 oran 87 . . . . . . . . . . 11 (a v b) = (a' ^ b')'
76ax-r1 35 . . . . . . . . . 10 (a' ^ b')' = (a v b)
85, 72an 79 . . . . . . . . 9 ((a' ^ b)' ^ (a' ^ b')') = ((a v b') ^ (a v b))
98ax-r4 37 . . . . . . . 8 ((a' ^ b)' ^ (a' ^ b')')' = ((a v b') ^ (a v b))'
103, 9ax-r2 36 . . . . . . 7 ((a' ^ b) v (a' ^ b')) = ((a v b') ^ (a v b))'
1110con2 67 . . . . . 6 ((a' ^ b) v (a' ^ b'))' = ((a v b') ^ (a v b))
12 df-a 40 . . . . . . . 8 (a ^ (a' v b)) = (a' v (a' v b)')'
13 anor1 88 . . . . . . . . . . 11 (a ^ b') = (a' v b)'
1413ax-r1 35 . . . . . . . . . 10 (a' v b)' = (a ^ b')
1514lor 70 . . . . . . . . 9 (a' v (a' v b)') = (a' v (a ^ b'))
1615ax-r4 37 . . . . . . . 8 (a' v (a' v b)')' = (a' v (a ^ b'))'
1712, 16ax-r2 36 . . . . . . 7 (a ^ (a' v b)) = (a' v (a ^ b'))'
1817con2 67 . . . . . 6 (a ^ (a' v b))' = (a' v (a ^ b'))
1911, 182an 79 . . . . 5 (((a' ^ b) v (a' ^ b'))' ^ (a ^ (a' v b))') = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
2019ax-r4 37 . . . 4 (((a' ^ b) v (a' ^ b'))' ^ (a ^ (a' v b))')' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))'
212, 20ax-r2 36 . . 3 (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))) = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))'
221, 21ax-r2 36 . 2 (a ->3 b) = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))'
2322con2 67 1 (a ->3 b)' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7   ->3 wi3 14
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-i3 46
This theorem is referenced by:  ud3lem0c  279
  Copyright terms: Public domain W3C validator