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

Definition df-xor 1221
Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with (wa 95), (wo 611), 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 1220 . 2 wff (φψ)
41, 2wo 611 . . 3 wff (φ ψ)
51, 2wa 95 . . . 4 wff (φ ψ)
65wn 3 . . 3 wff ¬ (φ ψ)
74, 6wa 95 . 2 wff ((φ ψ) ¬ (φ ψ))
83, 7wb 96 1 wff ((φψ) ↔ ((φ ψ) ¬ (φ ψ)))
Colors of variables: wff set class
This definition is referenced by:  xoranor  1222  xorbin  1224  xornbidc  1230  xordc1  1232  truxortru  1257  truxorfal  1258  falxortru  1259  falxorfal  1260  mpto2  1262  mtp-xor  1263
  Copyright terms: Public domain W3C validator