Axiom ax-int 208

Description: Generalization. An "anti variable abstraction" can be removed from a "top-level" wff. What does that even mean?

Hypothesis

Ref	Expression
ax-int.1	⊦ 𝜑

Assertion

Ref	Expression
ax-int	⊦ ~ νx~ 𝜑

Detailed syntax breakdown of Axiom ax-int

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2	1	wneg 3	. . 3 wff ~ 𝜑
3		vx	. . 3 var x
4	2, 3	wnu 206	. 2 wff νx~ 𝜑
5	4	wneg 3	1 wff ~ νx~ 𝜑

This axiom is referenced by: (None)