Definition df-nan 1522

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

This definition is referenced by:  nanan  1523  dfnan2  1524  nanor  1525  nanbi  1530  xornan2  1550  trunanfal  1612  nic-mpALT  1702  nic-ax  1703  nic-axALT  1704  nfnan  1930  elnanel  9572  naim1  36900  naim2  36901  df3nandALT1  36910  imnand2  36913  waj-ax  36925  lukshef-ax2  36926  arg-ax  36927  nandsym1  36933  tsna1  38793  tsna2  38794  tsna3  38795  ifpdfnan  44212  ifpnannanb  44233  nanorxor  45015  undisjrab  45016