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 1619
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 1641) and the constant false (df-fal 1651), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1683), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1684), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1685), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1686). Contrast with (df-an 385), (df-or 866), (wi 4), and (df-nan 1602). (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 1618 . 2 wff (𝜑𝜓)
41, 2wb 197 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 197 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1620  xorcom  1621  xorass  1622  excxor  1623  xor2  1624  xorneg2  1628  xorbi12i  1631  xorbi12d  1632  anxordi  1633  xorexmid  1634  truxortru  1683  truxorfal  1684  falxorfal  1686  hadbi  1692  elsymdifxor  4049  sadadd2lem2  15387  f1omvdco3  18066  tsxo3  34254  tsxo4  34255  ifpxorxorb  38353  or3or  38816  axorbtnotaiffb  41549  axorbciffatcxorb  41551  aisbnaxb  41557  abnotbtaxb  41561  abnotataxb  41562  afv2orxorb  41814
  Copyright terms: Public domain W3C validator