Theorem 19.9d

A deduction version of one direction of 19.9. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) Revised to shorten other proofs. (Revised by Wolf Lammen, 14-Jul-2020.) [df-nf] changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)

Hypothesis
19.9d.1
\( \vdash \psi \rightarrow \Finv x \, \varphi \)
Conclusion
\( \vdash \psi \rightarrow \exists x \, \varphi \rightarrow \varphi \)
Proof
19.9d.1
l1
nfrd _
\( \vdash \psi \rightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
sp
\( \vdash \forall x \, \varphi \rightarrow \varphi \)
syl6 l1 _