Theorem 19.9ht

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

Conclusion

\( \vdash \forall x \, (\varphi \rightarrow \forall x \, \varphi) \rightarrow \exists x \, \varphi \rightarrow \varphi \)

Proof

nf5-1

19.9d _