Axiom ax-nue 209

Description: A variable abstraction can be eliminated if the expression is free in that variable.

Assertion

Ref	Expression
ax-nue	⊦ (νx𝜑 ⊸ 𝜑)

Distinct variable group:   𝜑,x

Detailed syntax breakdown of Axiom ax-nue

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 var x
3	1, 2	wnu 206	. 2 wff νx𝜑
4	3, 1	wli 61	1 wff (νx𝜑 ⊸ 𝜑)

This axiom is referenced by: (None)