QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wwcomd Unicode version
Theorem wwcomd 214
Description: Commutation dual (weak). Kalmbach 83 p. 23.
Hypothesis
Ref Expression
wwcomd.1 a' C b
Assertion
Ref Expression
wwcomd a = ((a v b) ^ (a v b'))
Proof of Theorem wwcomd
StepHypRef Expression
1 wwcomd.1 . . . 4 a' C b
21df-c2 133 . . 3 a' = ((a' ^ b) v (a' ^ b'))
3 oran 87 . . . 4 ((a' ^ b') v (a' ^ b)) = ((a' ^ b')' ^ (a' ^ b)')'
4 ax-a2 31 . . . 4 ((a' ^ b) v (a' ^ b')) = ((a' ^ b') v (a' ^ b))
5 oran 87 . . . . . 6 (a v b) = (a' ^ b')'
6 anor2 89 . . . . . . . 8 (a' ^ b) = (a v b')'
76ax-r1 35 . . . . . . 7 (a v b')' = (a' ^ b)
87con3 68 . . . . . 6 (a v b') = (a' ^ b)'
95, 82an 79 . . . . 5 ((a v b) ^ (a v b')) = ((a' ^ b')' ^ (a' ^ b)')
109ax-r4 37 . . . 4 ((a v b) ^ (a v b'))' = ((a' ^ b')' ^ (a' ^ b)')'
113, 4, 103tr1 63 . . 3 ((a' ^ b) v (a' ^ b')) = ((a v b) ^ (a v b'))'
122, 11ax-r2 36 . 2 a' = ((a v b) ^ (a v b'))'
1312con1 66 1 a = ((a v b) ^ (a v b'))
Colors of variables: term
Syntax hints:   = wb 1   C wc 3  'wn 4   v wo 6   ^ wa 7
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-c2 133
This theorem is referenced by:  wwcom3ii  215
  Copyright terms: Public domain W3C validator