Definition df-nan 1487

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1489 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 1542) and the constant false ⊥ (df-fal 1552), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1580), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1581), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1582), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1583). Contrast with ∧ (df-an 397), ∨ (df-or 845), → (wi 4), and ⊻ (df-xor 1507). (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 1486	. 2 wff (𝜑 ⊼ 𝜓)
4	1, 2	wa 396	. . 3 wff (𝜑 ∧ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∧ 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is referenced by:  nanan  1488  dfnan2  1489  nanor  1490  nanbi  1495  xornan2  1516  trunanfal  1581  nic-mpALT  1675  nic-ax  1676  nic-axALT  1677  nfnan  1903  elnanel  9365  naim1  34578  naim2  34579  df3nandALT1  34588  imnand2  34591  waj-ax  34603  lukshef-ax2  34604  arg-ax  34605  nandsym1  34611  tsna1  36302  tsna2  36303  tsna3  36304  ifpdfnan  41093  ifpnannanb  41114  nanorxor  41923  undisjrab  41924