MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xor Structured version   Unicode version

Definition df-xor 1401
Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. After we define the constant true T. (df-tru 1440) and the constant false F. (df-fal 1443), we will be able to prove these truth table values:  ( ( T.  \/_ T.  ) 
<-> F.  ) (truxortru 1486), 
( ( T.  \/_ F.  )  <-> T.  ) (truxorfal 1487),  ( ( F.  \/_ T.  )  <-> T.  ) (falxortru 1488), and  ( ( F.  \/_ F.  )  <-> F.  ) (falxorfal 1490). Contrast with  /\ (df-an 372), 
\/ (df-or 371), 
-> (wi 4), and  -/\ (df-nan 1380) . (Contributed by FL, 22-Nov-2010.)
Assertion
Ref Expression
df-xor  |-  ( (
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 1400 . 2  wff  ( ph  \/_ 
ps )
41, 2wb 187 . . 3  wff  ( ph  <->  ps )
54wn 3 . 2  wff  -.  ( ph 
<->  ps )
63, 5wb 187 1  wff  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1402  xorcom  1403  xorass  1404  xorassOLD  1405  excxor  1406  xor2  1407  xorneg2  1411  xorneg1OLD  1413  xorbi12i  1416  xorbi12d  1417  anxordi  1418  xorexmid  1419  truxortru  1486  truxorfal  1487  falxortruOLD  1489  falxorfal  1490  hadbi  1496  sadadd2lem2  14387  f1omvdco3  17034  tsxo3  32085  tsxo4  32086  ifpxorxorb  35858  axorbtnotaiffb  37894  axorbciffatcxorb  37896  aisbnaxb  37902  abnotbtaxb  37907  abnotataxb  37908
  Copyright terms: Public domain W3C validator