Definition df-nan 1489

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1491 for an alternative. This is also called the Sheffer stroke, represented by a vertical bar, but we use a different symbol to avoid ambiguity with other uses of the vertical bar. In the second edition of Principia Mathematica (1927), Russell and Whitehead used the Sheffer stroke and suggested it as a replacement for the "or" and "not" operations of the first edition. However, in practice, "or" and "not" are more widely used. After we define the constant true ⊤ (df-tru 1543) and the constant false ⊥ (df-fal 1553), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1581), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1582), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1583), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1584). Contrast with ∧ (df-an 396), ∨ (df-or 845), → (wi 4), and ⊻ (df-xor 1509). (Contributed by Jeff Hoffman, 19-Nov-2007.)

Assertion

Ref	Expression
df-nan	⊢ ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

Detailed syntax breakdown of Definition df-nan

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wnan 1488	. 2 wff (𝜑 ⊼ 𝜓)
4	1, 2	wa 395	. . 3 wff (𝜑 ∧ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∧ 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is referenced by:  nanan  1490  dfnan2  1491  nanor  1492  nanbi  1497  xornan2  1518  trunanfal  1582  nic-mpALT  1673  nic-ax  1674  nic-axALT  1675  nfnan  1902  elnanel  9608  naim1  35737  naim2  35738  df3nandALT1  35747  imnand2  35750  waj-ax  35762  lukshef-ax2  35763  arg-ax  35764  nandsym1  35770  tsna1  37475  tsna2  37476  tsna3  37477  ifpdfnan  42699  ifpnannanb  42720  nanorxor  43526  undisjrab  43527