Definition df-nan 1512

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1514 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 1563) and the constant false ⊥ (df-fal 1573), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1601), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1602), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1603), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1604). Contrast with ∧ (df-an 400), ∨ (df-or 859), → (wi 4), and ⊻ (df-xor 1532). (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 1511	. 2 wff (𝜑 ⊼ 𝜓)
4	1, 2	wa 399	. . 3 wff (𝜑 ∧ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∧ 𝜓)
6	3, 5	wb 208	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is referenced by:  nanan  1513  dfnan2  1514  nanor  1515  nanbi  1520  xornan2  1540  trunanfal  1602  nic-mpALT  1692  nic-ax  1693  nic-axALT  1694  nfnan  1920  elnanel  9562  naim1  36749  naim2  36750  df3nandALT1  36759  imnand2  36762  waj-ax  36774  lukshef-ax2  36775  arg-ax  36776  nandsym1  36782  tsna1  38643  tsna2  38644  tsna3  38645  ifpdfnan  44062  ifpnannanb  44083  nanorxor  44881  undisjrab  44882