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 1540) and the constant false ⊥ (df-fal 1550), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1578), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1579), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1580), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1581). Contrast with ∧ (df-an 396), ∨ (df-or 847), → (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 206	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is referenced by:  nanan  1490  dfnan2  1491  nanor  1492  nanbi  1497  xornan2  1517  trunanfal  1579  nic-mpALT  1670  nic-ax  1671  nic-axALT  1672  nfnan  1899  elnanel  9676  naim1  36355  naim2  36356  df3nandALT1  36365  imnand2  36368  waj-ax  36380  lukshef-ax2  36381  arg-ax  36382  nandsym1  36388  tsna1  38104  tsna2  38105  tsna3  38106  ifpdfnan  43448  ifpnannanb  43469  nanorxor  44274  undisjrab  44275