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

Definition df-xor 1252
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 1251 . 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  1253  xorbi2d  1255  xorbi1d  1256  xorbin  1258  xorcom  1262  xornbidc  1265  xordc1  1267  anxordi  1274  truxortru  1293  truxorfal  1294  falxortru  1295  falxorfal  1296  mpto2  1298  mtp-xor  1299  bdxor  6412
  Copyright terms: Public domain W3C validator