Axiom ax-ref 211

Description: x is free in [a ≫ x].

Assertion

Ref	Expression
ax-ref	⊦ (νx[a ≫ x] 𝜑 ⊸ [a ≫ x] 𝜑)

Detailed syntax breakdown of Axiom ax-ref

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vx	. . . 4 var x
3		va	. . . . 5 var a
4	3	nvar 203	. . . 4 nilad a
5	1, 2, 4	wre 205	. . 3 wff [a ≫ x] 𝜑
6	5, 2	wnu 206	. 2 wff νx[a ≫ x] 𝜑
7	6, 5	wli 61	1 wff (νx[a ≫ x] 𝜑 ⊸ [a ≫ x] 𝜑)

This axiom is referenced by: (None)