Theorem nf5rd

Description: Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016)

	Ref	Expression
Hypothesis	nf5rd.1	$$⊢\phi \to Ⅎx\psi$$
Assertion	nf5rd	$$⊢\phi \to \left(\psi \to \forall x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nf5rd.1	$$⊢\phi \to Ⅎx\psi$$
2		nf5r	$$⊢Ⅎx\psi \to \left(\psi \to \forall x\psi \right)$$
3	1 2	syl	$$⊢\phi \to \left(\psi \to \forall x\psi \right)$$