QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-id5 Unicode version
Definition df-id5 1047
Description: Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
Assertion
Ref Expression
df-id5 (a ==5 b) = ((a ^ b) v (a' ^ b'))
Detailed syntax breakdown of Definition df-id5
StepHypRef Expression
1 wva . . 3 term a
2 wvb . . 3 term b
31, 2wid5 22 . 2 term (a ==5 b)
41, 2wa 7 . . 3 term (a ^ b)
51wn 4 . . . 4 term a'
62wn 4 . . . 4 term b'
75, 6wa 7 . . 3 term (a' ^ b')
84, 7wo 6 . 2 term ((a ^ b) v (a' ^ b'))
93, 8wb 1 1 wff (a ==5 b) = ((a ^ b) v (a' ^ b'))
Colors of variables: term
This definition is referenced by:  lem3.3.3lem1  1049  lem3.3.3lem2  1050  lem3.3.4  1053  lem3.3.7i5e1  1072  lem3.3.7i5e2  1073  lem3.4.3  1076  lem3.4.6  1079
  Copyright terms: Public domain W3C validator