Theorem 19.9ht

Description: A closed version of 19.9h . (Contributed by NM, 13-May-1993) (Proof shortened by Wolf Lammen, 3-Mar-2018)

	Ref	Expression
Assertion	19.9ht	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ∃ 𝑥 𝜑 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nf5-1	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → Ⅎ 𝑥 𝜑 )
2	1	19.9d	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ∃ 𝑥 𝜑 → 𝜑 ) )