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

Definition df-xor 1614
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 (df-tru 1635) and the constant false (df-fal 1638), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1677), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1678), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1679), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1680). Contrast with (df-an 385), (df-or 384), (wi 4), and (df-nan 1597) . (Contributed by FL, 22-Nov-2010.)
Assertion
Ref Expression
df-xor ((𝜑𝜓) ↔ ¬ (𝜑𝜓))

Detailed syntax breakdown of Definition df-xor
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wxo 1613 . 2 wff (𝜑𝜓)
41, 2wb 196 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 196 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1615  xorcom  1616  xorass  1617  excxor  1618  xor2  1619  xorneg2  1623  xorbi12i  1626  xorbi12d  1627  anxordi  1628  xorexmid  1629  truxortru  1677  truxorfal  1678  falxorfal  1680  hadbi  1686  sadadd2lem2  15395  f1omvdco3  18090  tsxo3  34278  tsxo4  34279  ifpxorxorb  38377  or3or  38840  axorbtnotaiffb  41595  axorbciffatcxorb  41597  aisbnaxb  41603  abnotbtaxb  41607  abnotataxb  41608
  Copyright terms: Public domain W3C validator