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 1640
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 1662) and the constant false (df-fal 1672), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1704), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1705), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1706), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1707). Contrast with (df-an 387), (df-or 881), (wi 4), and (df-nan 1615). (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 1639 . 2 wff (𝜑𝜓)
41, 2wb 198 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 198 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1641  xorcom  1642  xorass  1643  excxor  1644  xor2  1645  xorneg2  1649  xorbi12i  1652  xorbi12d  1653  anxordi  1654  xorexmid  1655  truxortru  1704  truxorfal  1705  falxorfal  1707  hadbi  1713  elsymdifxor  4078  sadadd2lem2  15546  f1omvdco3  18220  tsxo3  34487  tsxo4  34488  ifpxorxorb  38699  or3or  39160  axorbtnotaiffb  41865  axorbciffatcxorb  41867  aisbnaxb  41873  abnotbtaxb  41877  abnotataxb  41878  afv2orxorb  42131
  Copyright terms: Public domain W3C validator