Definition df-nan 1448

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

This definition is referenced by:  nanan  1449  nancom  1450  nannan  1451  nannot  1453  nanbi  1454  nanbi1  1455  xornan2  1473  trunanfal  1525  nic-mpALT  1597  nic-ax  1598  nic-axALT  1599  nfnan  1830  nfnanOLD  2238  naim1  32384  naim2  32385  df3nandALT1  32396  imnand2  32399  waj-ax  32413  lukshef-ax2  32414  arg-ax  32415  nandsym1  32421  wl-dfnan2  33296  tsna1  33951  tsna2  33952  tsna3  33953  ifpdfnan  37831  ifpnannanb  37852  nanorxor  38504  undisjrab  38505