Axiom ax-nnuf 212

Description: x is free in ~ νx𝜑. There's that weird "anti variable abstraction" again...

Assertion

Ref	Expression
ax-nnuf	⊦ (νx~ νx𝜑 ⊸ ~ νx𝜑)

Detailed syntax breakdown of Axiom ax-nnuf

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

This axiom is referenced by: (None)