Definition df-nan 1488

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 1526) and the constant false ⊥ (df-fal 1529), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1564), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1565), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1566), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1567). Contrast with ∧ (df-an 385), ∨ (df-or 384), → (wi 4), and ⊻ (df-xor 1505) . (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 1487	. 2 wff (𝜑 ⊼ 𝜓)
4	1, 2	wa 383	. . 3 wff (𝜑 ∧ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∧ 𝜓)
6	3, 5	wb 196	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is referenced by:  nanan  1489  nancom  1490  nannan  1491  nannot  1493  nanbi  1494  nanbi1  1495  xornan2  1513  trunanfal  1565  nic-mpALT  1637  nic-ax  1638  nic-axALT  1639  nfnan  1870  nfnanOLD  2274  naim1  32509  naim2  32510  df3nandALT1  32521  imnand2  32524  waj-ax  32538  lukshef-ax2  32539  arg-ax  32540  nandsym1  32546  wl-dfnan2  33426  tsna1  34081  tsna2  34082  tsna3  34083  ifpdfnan  38148  ifpnannanb  38169  nanorxor  38821  undisjrab  38822