Theorem nf5diOLD

Description: Obsolete version of nf5di as of 23-Oct-2026. (Contributed by NM, 17-Aug-2018) (Proof shortened by Wolf Lammen, 10-Jul-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nf5diOLD.1	$$⊢\phi \to Ⅎx\phi$$
2	1	nf5rd	$$⊢\phi \to \left(\phi \to \forall x\phi \right)$$
3	2	pm2.43i	$$⊢\phi \to \forall x\phi$$
4	3	nf5i	$$⊢Ⅎx\phi$$