Definition df-nan 1440

Description: Define incompatibility, or alternative denial ('not-and' or 'nand'). 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 1478) and the constant false ⊥ (df-fal 1481), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1515), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1516), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1517), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1518). Contrast with ∧ (df-an 385), ∨ (df-or 384), → (wi 4), and ⊻ (df-xor 1457) . (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 1439	. 2 wff (𝜑 ⊼ 𝜓)
4	1, 2	wa 383	. . 3 wff (𝜑 ∧ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∧ 𝜓)
6	3, 5	wb 195	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is referenced by:  nanan  1441  nancom  1442  nannan  1443  nannot  1445  nanbi  1446  nanbi1  1447  xornan2  1465  trunanfal  1516  nic-mpALT  1588  nic-ax  1589  nic-axALT  1590  nfnan  1818  nfnanOLD  2226  naim1  31554  naim2  31555  df3nandALT1  31566  imnand2  31569  waj-ax  31583  lukshef-ax2  31584  arg-ax  31585  nandsym1  31591  wl-dfnan2  32475  tsna1  33121  tsna2  33122  tsna3  33123  ifpdfnan  36850  ifpnannanb  36871  nanorxor  37526  undisjrab  37527