Definition df-nan 1492

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1494 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 1543) and the constant false ⊥ (df-fal 1553), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1581), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1582), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1583), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1584). Contrast with ∧ (df-an 396), ∨ (df-or 849), → (wi 4), and ⊻ (df-xor 1512). (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 1491	. 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  1493  dfnan2  1494  nanor  1495  nanbi  1500  xornan2  1520  trunanfal  1582  nic-mpALT  1672  nic-ax  1673  nic-axALT  1674  nfnan  1900  elnanel  9647  naim1  36390  naim2  36391  df3nandALT1  36400  imnand2  36403  waj-ax  36415  lukshef-ax2  36416  arg-ax  36417  nandsym1  36423  tsna1  38151  tsna2  38152  tsna3  38153  ifpdfnan  43499  ifpnannanb  43520  nanorxor  44324  undisjrab  44325