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

Definition df-xor 1283
Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with  /\ (wa 101),  \/ (wo 639), and  -> (wi 4) . (Contributed by FL, 22-Nov-2010.) (Modified by Jim Kingdon, 1-Mar-2018.)
Assertion
Ref Expression
df-xor  |-  ( (
ph  \/_  ps )  <->  ( ( ph  \/  ps )  /\  -.  ( ph  /\ 
ps ) ) )

Detailed syntax breakdown of Definition df-xor
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
31, 2wxo 1282 . 2  wff  ( ph  \/_ 
ps )
41, 2wo 639 . . 3  wff  ( ph  \/  ps )
51, 2wa 101 . . . 4  wff  ( ph  /\ 
ps )
65wn 3 . . 3  wff  -.  ( ph  /\  ps )
74, 6wa 101 . 2  wff  ( (
ph  \/  ps )  /\  -.  ( ph  /\  ps ) )
83, 7wb 102 1  wff  ( (
ph  \/_  ps )  <->  ( ( ph  \/  ps )  /\  -.  ( ph  /\ 
ps ) ) )
Colors of variables: wff set class
This definition is referenced by:  xoranor  1284  xorbi2d  1287  xorbi1d  1288  xorbin  1291  xorcom  1295  xornbidc  1298  xordc1  1300  anxordi  1307  truxortru  1326  truxorfal  1327  falxortru  1328  falxorfal  1329  mptxor  1331  reapltxor  7654  zeoxor  10180  odd2np1  10184  bdxor  10343
  Copyright terms: Public domain W3C validator