ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-xor Structured version   Unicode version

Definition df-xor 1266
Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with (wa 97), (wo 628), and (wi 4) . (Contributed by FL, 22-Nov-2010.) (Modified by Jim Kingdon, 1-Mar-2018.)
Assertion
Ref Expression
df-xor  \/_

Detailed syntax breakdown of Definition df-xor
StepHypRef Expression
1 wph . . 3
2 wps . . 3
31, 2wxo 1265 . 2  \/_
41, 2wo 628 . . 3
51, 2wa 97 . . . 4
65wn 3 . . 3
74, 6wa 97 . 2
83, 7wb 98 1  \/_
Colors of variables: wff set class
This definition is referenced by:  xoranor  1267  xorbi2d  1269  xorbi1d  1270  xorbin  1272  xorcom  1276  xornbidc  1279  xordc1  1281  anxordi  1288  truxortru  1307  truxorfal  1308  falxortru  1309  falxorfal  1310  mpto2  1312  mtp-xor  1313  reapltxor  7333  bdxor  9225
  Copyright terms: Public domain W3C validator