Definition df-nan 1484

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1486 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 1542) and the constant false ⊥ (df-fal 1552), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1580), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1581), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1582), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1583). Contrast with ∧ (df-an 396), ∨ (df-or 844), → (wi 4), and ⊻ (df-xor 1504). (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 1483	. 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  1485  dfnan2  1486  nanor  1487  nanbi  1492  xornan2  1513  trunanfal  1581  nic-mpALT  1676  nic-ax  1677  nic-axALT  1678  nfnan  1904  elnanel  9295  naim1  34505  naim2  34506  df3nandALT1  34515  imnand2  34518  waj-ax  34530  lukshef-ax2  34531  arg-ax  34532  nandsym1  34538  tsna1  36229  tsna2  36230  tsna3  36231  ifpdfnan  40991  ifpnannanb  41012  nanorxor  41812  undisjrab  41813