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

Definition df-xor 1249
Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with (wa 97), (wo 616), 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 1248 . 2 wff (φψ)
41, 2wo 616 . . 3 wff (φ ψ)
51, 2wa 97 . . . 4 wff (φ ψ)
65wn 3 . . 3 wff ¬ (φ ψ)
74, 6wa 97 . 2 wff ((φ ψ) ¬ (φ ψ))
83, 7wb 98 1 wff ((φψ) ↔ ((φ ψ) ¬ (φ ψ)))
Colors of variables: wff set class
This definition is referenced by:  xoranor  1250  xorbi2d  1252  xorbi1d  1253  xorbin  1255  xorcom  1259  xornbidc  1262  xordc1  1264  anxordi  1271  truxortru  1290  truxorfal  1291  falxortru  1292  falxorfal  1293  mpto2  1295  mtp-xor  1296
  Copyright terms: Public domain W3C validator