Definition df-nand 1230

Description: Define incompatibility ('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.

Assertion

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

Detailed syntax breakdown of Definition df-nand

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3	1, 2	wnand 1229	. 2 wff (ph -/\ ps)
4	1, 2	wa 240	. . 3 wff (ph /\ ps)
5	4	wn 2	. 2 wff -. (ph /\ ps)
6	3, 5	wb 163	1 wff ((ph -/\ ps) <-> -. (ph /\ ps))

This definition is referenced by:  nic-justlem 1231  nic-justneg 1233  nic-justbi 1234  nic-mpALT 1238  nic-ax 1239  nic-axALT 1240  TFSid 14125  FTSid 14126  naim1 14134  naim2 14135  nabi1 14139  nabi2 14140  df3nandALT1 14146  imnand2 14149  waj-ax 14238  lukshef-ax2 14239  arg-ax 14240  nandsym1 14246

Copyright terms: Public domain