QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-id4oa GIF version

Definition df-id4oa 58
Description: The 4-variable orthoarguesian identity term. (Contributed by NM, 28-Nov-1998.)
Assertion
Ref Expression
df-id4oa (ac, dOA b) = ((adOA b) ∪ ((adOA c) ∩ (bdOA 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  (ac, dOA b)
61, 2, 4wid3oa 27 . . 3 term  (adOA b)
71, 3, 4wid3oa 27 . . . 4 term  (adOA c)
82, 3, 4wid3oa 27 . . . 4 term  (bdOA c)
97, 8wa 7 . . 3 term  ((adOA c) ∩ (bdOA c))
106, 9wo 6 . 2 term  ((adOA b) ∪ ((adOA c) ∩ (bdOA c)))
115, 10wb 1 1 wff  (ac, dOA b) = ((adOA b) ∪ ((adOA c) ∩ (bdOA c)))
Colors of variables: term
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator