Definition df-nan 1488

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1490 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 1539) and the constant false ⊥ (df-fal 1549), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1577), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1578), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1579), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1580). Contrast with ∧ (df-an 396), ∨ (df-or 848), → (wi 4), and ⊻ (df-xor 1508). (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 1487	. 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  1489  dfnan2  1490  nanor  1491  nanbi  1496  xornan2  1516  trunanfal  1578  nic-mpALT  1668  nic-ax  1669  nic-axALT  1670  nfnan  1897  elnanel  9644  naim1  36371  naim2  36372  df3nandALT1  36381  imnand2  36384  waj-ax  36396  lukshef-ax2  36397  arg-ax  36398  nandsym1  36404  tsna1  38130  tsna2  38131  tsna3  38132  ifpdfnan  43475  ifpnannanb  43496  nanorxor  44300  undisjrab  44301