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 1511
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 1542) and the constant false (df-fal 1552), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1584), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1585), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1586), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1587). Contrast with (df-an 396), (df-or 848), (wi 4), and (df-nan 1491). (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 1510 . 2 wff (𝜑𝜓)
41, 2wb 206 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 206 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1512  xorcom  1513  xorass  1514  excxor  1515  xor2  1516  xorneg2  1520  xorbi12i  1523  xorbi12d  1524  anxordi  1525  xorexmid  1526  truxortru  1584  truxorfal  1585  falxorfal  1587  hadbi  1597  elsymdifxor  4259  sadadd2lem2  16488  f1omvdco3  19468  bj-bixor  36593  wl-df3xor2  37471  wl-3xorbi  37475  wl-2xor  37485  tsxo3  38147  tsxo4  38148  oneptri  43274  ifpxorxorb  43529  or3or  44041  axorbtnotaiffb  46920  axorbciffatcxorb  46922  aisbnaxb  46928  abnotbtaxb  46932  abnotataxb  46933  afv2orxorb  47245
  Copyright terms: Public domain W3C validator