Definition df-nan 1481

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 1536) and the constant false ⊥ (df-fal 1546), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1574), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1575), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1576), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1577). Contrast with ∧ (df-an 399), ∨ (df-or 844), → (wi 4), and ⊻ (df-xor 1501). (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 1480	. 2 wff (𝜑 ⊼ 𝜓)
4	1, 2	wa 398	. . 3 wff (𝜑 ∧ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∧ 𝜓)
6	3, 5	wb 208	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is referenced by:  nanan  1482  nanimn  1483  nanor  1484  nanbi  1489  xornan2  1509  trunanfal  1575  nic-mpALT  1669  nic-ax  1670  nic-axALT  1671  nfnan  1897  elnanel  9069  naim1  33737  naim2  33738  df3nandALT1  33747  imnand2  33750  waj-ax  33762  lukshef-ax2  33763  arg-ax  33764  nandsym1  33770  tsna1  35421  tsna2  35422  tsna3  35423  ifpdfnan  39850  ifpnannanb  39871  nanorxor  40635  undisjrab  40636