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

Definition df-xor 1308
Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with (wa 102), (wo 662), 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 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wxo 1307 . 2 wff (𝜑𝜓)
41, 2wo 662 . . 3 wff (𝜑𝜓)
51, 2wa 102 . . . 4 wff (𝜑𝜓)
65wn 3 . . 3 wff ¬ (𝜑𝜓)
74, 6wa 102 . 2 wff ((𝜑𝜓) ∧ ¬ (𝜑𝜓))
83, 7wb 103 1 wff ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ ¬ (𝜑𝜓)))
Colors of variables: wff set class
This definition is referenced by:  xoranor  1309  xorbi2d  1312  xorbi1d  1313  xorbin  1316  xorcom  1320  xornbidc  1323  xordc1  1325  anxordi  1332  truxortru  1351  truxorfal  1352  falxortru  1353  falxorfal  1354  mptxor  1356  reapltxor  7965  zeoxor  10648  odd2np1  10652  bdxor  11069
  Copyright terms: Public domain W3C validator