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

Definition df-id3oa 57
 Description: The 3-variable orthoarguesian identity term. (Contributed by NM, 22-Sep-1998.)
Assertion
Ref Expression
df-id3oa (acOA b) = (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))

Detailed syntax breakdown of Definition df-id3oa
StepHypRef Expression
1 wva . . 3 term  a
2 wvb . . 3 term  b
3 wvc . . 3 term  c
41, 2, 3wid3oa 27 . 2 term  (acOA b)
51, 3wi1 12 . . . 4 term  (a1 c)
62, 3wi1 12 . . . 4 term  (b1 c)
75, 6wa 7 . . 3 term  ((a1 c) ∩ (b1 c))
81wn 4 . . . . 5 term  a
98, 3wi1 12 . . . 4 term  (a1 c)
102wn 4 . . . . 5 term  b
1110, 3wi1 12 . . . 4 term  (b1 c)
129, 11wa 7 . . 3 term  ((a1 c) ∩ (b1 c))
137, 12wo 6 . 2 term  (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))
144, 13wb 1 1 wff  (acOA b) = (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))
 Colors of variables: term This definition is referenced by:  3oa3  1025
 Copyright terms: Public domain W3C validator