wne - Linear Logic Proof Explorer

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

Syntax Definition wne 48

Description: "Why not", negative exponential. Characterized by ax-ipe 49, ax-epe 50, ax-weak 51, ax-contr 52, ax-pemc 53, ax-dig 54.

**Hypothesis**
Ref	Expression
wph	wff 𝜑

**Assertion**
Ref	Expression
wne	wff ? 𝜑

This syntax is primitive. The first axiom using it is ax-ipe 49.

Colors of variables: wff var nilad