Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xor Structured version   Visualization version   GIF version

Definition df-xor 1463
 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 1484) and the constant false ⊥ (df-fal 1487), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1526), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1527), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1528), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1529). Contrast with ∧ (df-an 386), ∨ (df-or 385), → (wi 4), and ⊼ (df-nan 1446) . (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 1462 . 2 wff (𝜑𝜓)
41, 2wb 196 . . 3 wff (𝜑𝜓)
54wn 3 . 2 wff ¬ (𝜑𝜓)
63, 5wb 196 1 wff ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class This definition is referenced by:  xnor  1464  xorcom  1465  xorass  1466  excxor  1467  xor2  1468  xorneg2  1472  xorbi12i  1475  xorbi12d  1476  anxordi  1477  xorexmid  1478  truxortru  1526  truxorfal  1527  falxorfal  1529  hadbi  1535  sadadd2lem2  15153  f1omvdco3  17850  tsxo3  33917  tsxo4  33918  ifpxorxorb  37675  or3or  38139  axorbtnotaiffb  40833  axorbciffatcxorb  40835  aisbnaxb  40841  abnotbtaxb  40845  abnotataxb  40846
 Copyright terms: Public domain W3C validator