Definition df-nan 1521

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1523 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 1572) and the constant false ⊥ (df-fal 1582), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1610), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1611), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1612), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1613). Contrast with ∧ (df-an 402), ∨ (df-or 862), → (wi 4), and ⊻ (df-xor 1541). (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 1520	. 2 wff (𝜑 ⊼ 𝜓)
4	1, 2	wa 401	. . 3 wff (𝜑 ∧ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∧ 𝜓)
6	3, 5	wb 209	1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

This definition is used by:  nanan  1522  dfnan2  1523  nanor  1524  nanbi  1529  xornan2  1549  trunanfal  1611  nic-mpALT  1704  nic-ax  1705  nic-axALT  1706  nfnan  1932  elnanel  9615  naim1  37301  naim2  37302  df3nandALT1  37311  imnand2  37314  waj-ax  37326  lukshef-ax2  37327  arg-ax  37328  nandsym1  37334  tsna1  39213  tsna2  39214  tsna3  39215  ifpdfnan  44624  ifpnannanb  44645  nanorxor  45426  undisjrab  45427