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 1496
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 1531) and the constant false (df-fal 1541), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1573), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1574), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1575), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1576). Contrast with (df-an 397), (df-or 842), (wi 4), and (df-nan 1476). (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 1495 . 2 wff (𝜑𝜓)
41, 2wb 207 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 207 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1497  xorcom  1498  xorass  1499  excxor  1500  xor2  1501  xorneg2  1505  xorbi12i  1508  xorbi12d  1509  anxordi  1510  xorexmid  1511  truxortru  1573  truxorfal  1574  falxorfal  1576  hadbi  1589  elsymdifxor  4225  sadadd2lem2  15789  f1omvdco3  18508  bj-bixor  33823  tsxo3  35300  tsxo4  35301  ifpxorxorb  39757  or3or  40251  axorbtnotaiffb  43020  axorbciffatcxorb  43022  aisbnaxb  43028  abnotbtaxb  43032  abnotataxb  43033  afv2orxorb  43308
  Copyright terms: Public domain W3C validator