Definition df-nan 1494

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1496 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 396), ∨ (df-or 849), → (wi 4), and ⊻ (df-xor 1514). (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 1493	. 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  1495  dfnan2  1496  nanor  1497  nanbi  1502  xornan2  1522  trunanfal  1584  nic-mpALT  1674  nic-ax  1675  nic-axALT  1676  nfnan  1902  elnanel  9522  naim1  36590  naim2  36591  df3nandALT1  36600  imnand2  36603  waj-ax  36615  lukshef-ax2  36616  arg-ax  36617  nandsym1  36623  tsna1  38482  tsna2  38483  tsna3  38484  ifpdfnan  43934  ifpnannanb  43955  nanorxor  44753  undisjrab  44754