QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wdcom Unicode version
Theorem wdcom 1103
Description: Any two variables (weakly) commute in a WDOL.
Assertion
Ref Expression
wdcom C (a, b) = 1
Proof of Theorem wdcom
StepHypRef Expression
1 df-cmtr 134 . 2 C (a, b) = (((a ^ b) v (a ^ b')) v ((a' ^ b) v (a' ^ b')))
2 or42 85 . 2 (((a ^ b) v (a ^ b')) v ((a' ^ b) v (a' ^ b'))) = (((a ^ b) v (a' ^ b')) v ((a ^ b') v (a' ^ b)))
3 dfb 94 . . . . 5 (a == b) = ((a ^ b) v (a' ^ b'))
4 dfb 94 . . . . . 6 (a == b') = ((a ^ b') v (a' ^ b''))
5 ax-a1 30 . . . . . . . . 9 b = b''
65lan 77 . . . . . . . 8 (a' ^ b) = (a' ^ b'')
76ax-r1 35 . . . . . . 7 (a' ^ b'') = (a' ^ b)
87lor 70 . . . . . 6 ((a ^ b') v (a' ^ b'')) = ((a ^ b') v (a' ^ b))
94, 8ax-r2 36 . . . . 5 (a == b') = ((a ^ b') v (a' ^ b))
103, 92or 72 . . . 4 ((a == b) v (a == b')) = (((a ^ b) v (a' ^ b')) v ((a ^ b') v (a' ^ b)))
1110ax-r1 35 . . 3 (((a ^ b) v (a' ^ b')) v ((a ^ b') v (a' ^ b))) = ((a == b) v (a == b'))
12 ax-wdol 1102 . . 3 ((a == b) v (a == b')) = 1
1311, 12ax-r2 36 . 2 (((a ^ b) v (a' ^ b')) v ((a ^ b') v (a' ^ b))) = 1
141, 2, 133tr 65 1 C (a, b) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8   C wcmtr 29
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-wdol 1102
This theorem depends on definitions:  df-b 39  df-a 40  df-cmtr 134
This theorem is referenced by:  wdwom  1104  wddi1  1105  wddi3  1107
  Copyright terms: Public domain W3C validator