This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \forall x (φ \to \forall x φ) \to (\exists x φ \to φ)$

Step	Hyp	Ref	Expression
1		nf5-1	$⊢ \forall x (φ \to \forall x φ) \to Ⅎ x φ$
2	1	19.9d	$⊢ \forall x (φ \to \forall x φ) \to (\exists x φ \to φ)$