Definition df-nan 1493

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1495 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 396), ∨ (df-or 848), → (wi 4), and ⊻ (df-xor 1513). (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 1492	. 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  1494  dfnan2  1495  nanor  1496  nanbi  1501  xornan2  1521  trunanfal  1583  nic-mpALT  1673  nic-ax  1674  nic-axALT  1675  nfnan  1901  elnanel  9516  naim1  36583  naim2  36584  df3nandALT1  36593  imnand2  36596  waj-ax  36608  lukshef-ax2  36609  arg-ax  36610  nandsym1  36616  tsna1  38345  tsna2  38346  tsna3  38347  ifpdfnan  43727  ifpnannanb  43748  nanorxor  44546  undisjrab  44547