Definition df-nan 1342

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 T. (df-tru 1401) and the constant false F. (df-fal 1404), we will be able to prove these truth table values: ( ( T. -/\ T. ) <-> F. ) (trunantru 1440), ( ( T. -/\ F. ) <-> T. ) (trunanfal 1441), ( ( F. -/\ T. ) <-> T. ) (falnantru 1442), and ( ( F. -/\ F. ) <-> T. ) (falnanfal 1443). Contrast with /\ (df-an 369), \/ (df-or 368), -> (wi 4), and \/_ (df-xor 1363) . (Contributed by Jeff Hoffman, 19-Nov-2007.)

Assertion

Ref	Expression
df-nan	|- ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )

Detailed syntax breakdown of Definition df-nan

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3	1, 2	wnan 1341	. 2 wff ( ph -/\ ps )
4	1, 2	wa 367	. . 3 wff ( ph /\ ps )
5	4	wn 3	. 2 wff -. ( ph /\ ps )
6	3, 5	wb 184	1 wff ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )

This definition is referenced by:  nanan  1343  nancom  1344  nancomOLD  1345  nannan  1346  nannanOLD  1347  nannot  1349  nanbi  1350  nanbiOLD  1351  nanbiOLDOLD  1352  nanbi1  1353  xornan2  1372  trunanfal  1441  nic-mpALT  1509  nic-ax  1510  nic-axALT  1511  nfnan  1934  naim1  30078  naim2  30079  df3nandALT1  30090  imnand2  30093  waj-ax  30107  lukshef-ax2  30108  arg-ax  30109  nandsym1  30115  wl-dfnan2  30211  tsna1  30791  tsna2  30792  tsna3  30793  nanorxor  31426  undisjrab  31427  ifpdfnan  38148  ifpnannanb  38149