Theorem bj-nfdt0

Description: A theorem close to a closed form of nf5d and nf5dh . (Contributed by BJ, 2-May-2019)

	Ref	Expression
Assertion	bj-nfdt0	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ( ∀ 𝑥 𝜑 → Ⅎ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		alim	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) )
2		nf5	⊢ ( Ⅎ 𝑥 𝜓 ↔ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) )
3	1 2	syl6ibr	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ( ∀ 𝑥 𝜑 → Ⅎ 𝑥 𝜓 ) )