Definition df-nan 1491

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1493 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 1545) and the constant false ⊥ (df-fal 1555), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1583), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1584), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1585), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1586). Contrast with ∧ (df-an 398), ∨ (df-or 847), → (wi 4), and ⊻ (df-xor 1511). (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 1490	. 2 wff (𝜑 ⊼ 𝜓)
4	1, 2	wa 397	. . 3 wff (𝜑 ∧ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∧ 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is referenced by:  nanan  1492  dfnan2  1493  nanor  1494  nanbi  1499  xornan2  1520  trunanfal  1584  nic-mpALT  1675  nic-ax  1676  nic-axALT  1677  nfnan  1904  elnanel  9602  naim1  35322  naim2  35323  df3nandALT1  35332  imnand2  35335  waj-ax  35347  lukshef-ax2  35348  arg-ax  35349  nandsym1  35355  tsna1  37060  tsna2  37061  tsna3  37062  ifpdfnan  42285  ifpnannanb  42306  nanorxor  43112  undisjrab  43113