ax-nuf - Linear Logic Proof Explorer

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

Axiom ax-nuf 210

Description: x is free in νx.

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

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

Colors of variables: wff var nilad

This axiom is referenced by: (None)