Theorem nf5ri

Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 15-Mar-2023)

	Ref	Expression
Hypothesis	nf5ri.1	$$⊢Ⅎx\phi$$
Assertion	nf5ri	$$⊢\phi \to \forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		nf5ri.1	$$⊢Ⅎx\phi$$
2	1	nfri	$$⊢\exists x\phi \to \forall x\phi$$
3	2	19.23bi	$$⊢\phi \to \forall x\phi$$