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

Definition df-xor 1355
 Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with ∧ (wa 103), ∨ (wo 698), 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 1354 . 2 wff (𝜑𝜓)
41, 2wo 698 . . 3 wff (𝜑𝜓)
51, 2wa 103 . . . 4 wff (𝜑𝜓)
65wn 3 . . 3 wff ¬ (𝜑𝜓)
74, 6wa 103 . 2 wff ((𝜑𝜓) ∧ ¬ (𝜑𝜓))
83, 7wb 104 1 wff ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ ¬ (𝜑𝜓)))
 Colors of variables: wff set class This definition is referenced by:  xoranor  1356  xorbi2d  1359  xorbi1d  1360  xorbin  1363  xorcom  1367  xornbidc  1370  xordc1  1372  anxordi  1379  truxortru  1398  truxorfal  1399  falxortru  1400  falxorfal  1401  mptxor  1403  reapltxor  8402  zeoxor  11636  odd2np1  11640  bdxor  13249  trirec0xor  13458
 Copyright terms: Public domain W3C validator