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	⊢ Ⅎ 𝑥 𝜑
Assertion	nf5ri	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nf5ri.1	⊢ Ⅎ 𝑥 𝜑
2	1	nfri	⊢ ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 )
3	2	19.23bi	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )