QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-id4oa Unicode version
Definition df-id4oa 58
Description: The 4-variable orthoarguesian identity term.
Assertion
Ref Expression
df-id4oa (a == c, d ==OA b) = ((a == d ==OA b) v ((a == d ==OA c) ^ (b == d ==OA c)))
Detailed syntax breakdown of Definition df-id4oa
StepHypRef Expression
1 wva . . 3 term a
2 wvb . . 3 term b
3 wvc . . 3 term c
4 wvd . . 3 term d
51, 2, 3, 4wid4oa 28 . 2 term (a == c, d ==OA b)
61, 2, 4wid3oa 27 . . 3 term (a == d ==OA b)
71, 3, 4wid3oa 27 . . . 4 term (a == d ==OA c)
82, 3, 4wid3oa 27 . . . 4 term (b == d ==OA c)
97, 8wa 7 . . 3 term ((a == d ==OA c) ^ (b == d ==OA c))
106, 9wo 6 . 2 term ((a == d ==OA b) v ((a == d ==OA c) ^ (b == d ==OA c)))
115, 10wb 1 1 wff (a == c, d ==OA b) = ((a == d ==OA b) v ((a == d ==OA c) ^ (b == d ==OA c)))
Colors of variables: term
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator