ax-nui - Linear Logic Proof Explorer

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

Axiom ax-nui 213

Description: A wff can be surrounded by a variable abstraction

**Assertion**
Ref	Expression
ax-nui	⊦ (𝜑 ⊸ νx𝜑)

**Detailed syntax breakdown of Axiom ax-nui**
Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		vx	. . 3 var x
3	1, 2	wnu 206	. 2 wff νx𝜑
4	1, 3	wli 61	1 wff (𝜑 ⊸ νx𝜑)

Colors of variables: wff var nilad

This axiom is referenced by: (None)