wnf - Linear Logic Proof Explorer

	Linear Logic Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > LLPE Home > Th. List > wnf		Structured version

Syntax Definition wnf 320

Description: Not-free predicate. Defined by df-nf 335.

**Hypotheses**
Ref	Expression
wph	wff 𝜑
vx	var x

**Assertion**
Ref	Expression
wnf	wff Ⅎx𝜑

See definition df-nf 335 for more information.

Colors of variables: wff var nilad