Definition df-nan 1519

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1521 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 1570) and the constant false ⊥ (df-fal 1580), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1608), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1609), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1610), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1611). Contrast with ∧ (df-an 401), ∨ (df-or 861), → (wi 4), and ⊻ (df-xor 1539). (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 1518	. 2 wff (𝜑 ⊼ 𝜓)
4	1, 2	wa 400	. . 3 wff (𝜑 ∧ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∧ 𝜓)
6	3, 5	wb 209	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is referenced by:  nanan  1520  dfnan2  1521  nanor  1522  nanbi  1527  xornan2  1547  trunanfal  1609  nic-mpALT  1699  nic-ax  1700  nic-axALT  1701  nfnan  1927  elnanel  9575  naim1  36788  naim2  36789  df3nandALT1  36798  imnand2  36801  waj-ax  36813  lukshef-ax2  36814  arg-ax  36815  nandsym1  36821  tsna1  38682  tsna2  38683  tsna3  38684  ifpdfnan  44103  ifpnannanb  44124  nanorxor  44906  undisjrab  44907