Definition df-nan

Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 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 T. ( df-tru ) and the constant false F. ( df-fal ), we will be able to prove these truth table values: ( ( T. -/\ T. ) <-> F. ) ( trunantru ), ( ( T. -/\ F. ) <-> T. ) ( trunanfal ), ( ( F. -/\ T. ) <-> T. ) ( falnantru ), and ( ( F. -/\ F. ) <-> T. ) ( falnanfal ). Contrast with /\ ( df-an ), \/ ( df-or ), -> ( wi ), and \/_ ( df-xor ). (Contributed by Jeff Hoffman, 19-Nov-2007)

	Ref	Expression
Assertion	df-nan	$$⊢\left(\phi ⊼\psi \right)\leftrightarrow \neg \left(\phi \wedge \psi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2	0 1	wnan	$$wff\left(\phi ⊼\psi \right)$$
3	0 1	wa	$$wff\left(\phi \wedge \psi \right)$$
4	3	wn	$$wff\neg \left(\phi \wedge \psi \right)$$
5	2 4	wb	$$wff\left(\left(\phi ⊼\psi \right)\leftrightarrow \neg \left(\phi \wedge \psi \right)\right)$$