Definition df-nan 1288

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 1319) and the constant false ⊥ (df-fal 1320), we will be able to prove these truth table values: (( ⊤ ⊼ ⊤ ) ↔ ⊥ ) (trunantru 1354), (( ⊤ ⊼ ⊥ ) ↔ ⊤ ) (trunanfal 1355), (( ⊥ ⊼ ⊤ ) ↔ ⊤ ) (falnantru 1356), and (( ⊥ ⊼ ⊥ ) ↔ ⊤ ) (falnanfal 1357). Contrast with ∧ (df-an 360), ∨ (df-or 359), → (wi 4), and ⊻ (df-xor 1305) . (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 1287	. 2 wff (φ ⊼ ψ)
4	1, 2	wa 358	. . 3 wff (φ ∧ ψ)
5	4	wn 3	. 2 wff ¬ (φ ∧ ψ)
6	3, 5	wb 176	1 wff ((φ ⊼ ψ) ↔ ¬ (φ ∧ ψ))

This definition is referenced by:  nanan  1289  nancom  1290  nannan  1291  nannot  1293  nanbi  1294  nanbi1  1295  trunanfal  1355  nic-mpALT  1437  nic-ax  1438  nic-axALT  1439  nfnan  1825  elcomplg  3219  elin  3220  elun  3221  nincompl  4073