QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  i3n1 Unicode version
Theorem i3n1 249
Description: Equivalence for Kalmbach implication.
Assertion
Ref Expression
i3n1 (a' ->3 b') = (((a ^ b') v (a ^ b)) v (a' ^ (a v b')))
Proof of Theorem i3n1
StepHypRef Expression
1 df-i3 46 . 2 (a' ->3 b') = (((a'' ^ b') v (a'' ^ b'')) v (a' ^ (a'' v b')))
2 ax-a1 30 . . . . . 6 a = a''
32ran 78 . . . . 5 (a ^ b') = (a'' ^ b')
4 ax-a1 30 . . . . . 6 b = b''
52, 42an 79 . . . . 5 (a ^ b) = (a'' ^ b'')
63, 52or 72 . . . 4 ((a ^ b') v (a ^ b)) = ((a'' ^ b') v (a'' ^ b''))
72ax-r5 38 . . . . 5 (a v b') = (a'' v b')
87lan 77 . . . 4 (a' ^ (a v b')) = (a' ^ (a'' v b'))
96, 82or 72 . . 3 (((a ^ b') v (a ^ b)) v (a' ^ (a v b'))) = (((a'' ^ b') v (a'' ^ b'')) v (a' ^ (a'' v b')))
109ax-r1 35 . 2 (((a'' ^ b') v (a'' ^ b'')) v (a' ^ (a'' v b'))) = (((a ^ b') v (a ^ b)) v (a' ^ (a v b')))
111, 10ax-r2 36 1 (a' ->3 b') = (((a ^ b') v (a ^ b)) v (a' ^ (a v 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:  oi3ai3  503  i3con  551  i3orlem7  558  i3orlem8  559
  Copyright terms: Public domain W3C validator