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 1456
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 1477) and the constant false (df-fal 1480), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1518), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1519), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1520), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1521). Contrast with (df-an 384), (df-or 383), (wi 4), and (df-nan 1439) . (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 1455 . 2 wff (𝜑𝜓)
41, 2wb 194 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 194 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1457  xorcom  1458  xorass  1459  excxor  1460  xor2  1461  xorneg2  1465  xorbi12i  1468  xorbi12d  1469  anxordi  1470  xorexmid  1471  truxortru  1518  truxorfal  1519  falxorfal  1521  hadbi  1527  sadadd2lem2  14952  f1omvdco3  17634  tsxo3  32915  tsxo4  32916  ifpxorxorb  36674  or3or  37138  axorbtnotaiffb  39519  axorbciffatcxorb  39521  aisbnaxb  39527  abnotbtaxb  39531  abnotataxb  39532
  Copyright terms: Public domain W3C validator