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

Definition df-xor 1266
Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with (wa 97), (wo 628), 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 1265 . 2 wff (φψ)
41, 2wo 628 . . 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  1267  xorbi2d  1269  xorbi1d  1270  xorbin  1272  xorcom  1276  xornbidc  1279  xordc1  1281  anxordi  1288  truxortru  1307  truxorfal  1308  falxortru  1309  falxorfal  1310  mpto2  1312  mtp-xor  1313  reapltxor  7325  bdxor  8890
  Copyright terms: Public domain W3C validator