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

Proof

Step	Hyp	Ref	Expression
1		nf5diOLD.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝜑 )
2	1	nf5rd	⊢ ( 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) )
3	2	pm2.43i	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
4	3	nf5i	⊢ Ⅎ 𝑥 𝜑