Definition df-nan 1380

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 1440) and the constant false F. (df-fal 1443), we will be able to prove these truth table values: ( ( T. -/\ T. ) <-> F. ) (trunantru 1481), ( ( T. -/\ F. ) <-> T. ) (trunanfal 1482), ( ( F. -/\ T. ) <-> T. ) (falnantru 1484), and ( ( F. -/\ F. ) <-> T. ) (falnanfal 1485). Contrast with /\ (df-an 372), \/ (df-or 371), -> (wi 4), and \/_ (df-xor 1401) . (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 1379	. 2 wff ( ph -/\ ps )
4	1, 2	wa 370	. . 3 wff ( ph /\ ps )
5	4	wn 3	. 2 wff -. ( ph /\ ps )
6	3, 5	wb 187	1 wff ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )

This definition is referenced by:  nanan  1381  nancom  1382  nancomOLD  1383  nannan  1384  nannanOLD  1385  nannot  1387  nanbi  1388  nanbiOLD  1389  nanbiOLDOLD  1390  nanbi1  1391  xornan2  1410  trunanfal  1482  trunanfalOLD  1483  nic-mpALT  1551  nic-ax  1552  nic-axALT  1553  nfnan  1987  naim1  30830  naim2  30831  df3nandALT1  30842  imnand2  30845  waj-ax  30859  lukshef-ax2  30860  arg-ax  30861  nandsym1  30867  wl-dfnan2  31558  tsna1  32090  tsna2  32091  tsna3  32092  ifpdfnan  35829  ifpnannanb  35850  nanorxor  36290  undisjrab  36291