Definition df-nan 1490

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

This definition is referenced by:  nanan  1491  dfnan2  1492  nanor  1493  nanbi  1498  xornan2  1519  trunanfal  1583  nic-mpALT  1674  nic-ax  1675  nic-axALT  1676  nfnan  1903  elnanel  9552  naim1  34937  naim2  34938  df3nandALT1  34947  imnand2  34950  waj-ax  34962  lukshef-ax2  34963  arg-ax  34964  nandsym1  34970  tsna1  36676  tsna2  36677  tsna3  36678  ifpdfnan  41880  ifpnannanb  41901  nanorxor  42707  undisjrab  42708