Definition df-nan 1499

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1501 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 1550) and the constant false ⊥ (df-fal 1560), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1588), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1589), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1590), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1591). Contrast with ∧ (df-an 397), ∨ (df-or 854), → (wi 4), and ⊻ (df-xor 1519). (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 1498	. 2 wff (𝜑 ⊼ 𝜓)
4	1, 2	wa 396	. . 3 wff (𝜑 ∧ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∧ 𝜓)
6	3, 5	wb 207	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is referenced by:  nanan  1500  dfnan2  1501  nanor  1502  nanbi  1507  xornan2  1527  trunanfal  1589  nic-mpALT  1679  nic-ax  1680  nic-axALT  1681  nfnan  1907  elnanel  9519  naim1  36617  naim2  36618  df3nandALT1  36627  imnand2  36630  waj-ax  36642  lukshef-ax2  36643  arg-ax  36644  nandsym1  36650  tsna1  38511  tsna2  38512  tsna3  38513  ifpdfnan  43930  ifpnannanb  43951  nanorxor  44749  undisjrab  44750