QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-id3 Unicode version
Definition df-id3 52
Description: Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
Assertion
Ref Expression
df-id3 (a ==3 b) = ((a' v b) ^ (a v (a' ^ b')))
Detailed syntax breakdown of Definition df-id3
StepHypRef Expression
1 wva . . 3 term a
2 wvb . . 3 term b
31, 2wid3 20 . 2 term (a ==3 b)
41wn 4 . . . 4 term a'
54, 2wo 6 . . 3 term (a' v b)
62wn 4 . . . . 5 term b'
74, 6wa 7 . . . 4 term (a' ^ b')
81, 7wo 6 . . 3 term (a v (a' ^ b'))
95, 8wa 7 . 2 term ((a' v b) ^ (a v (a' ^ b')))
103, 9wb 1 1 wff (a ==3 b) = ((a' v b) ^ (a v (a' ^ b')))
Colors of variables: term
This definition is referenced by:  nomb32  300  nom23  316  nom54  335  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  wdid0id3  1112
  Copyright terms: Public domain W3C validator