Theorem nf5di

Since the converse holds by a1i, this inference shows that we can represent a not-free hypothesis with either \( \Finv x \, \varphi \) (inference form) or \( \varphi \rightarrow \Finv x \, \varphi \) (deduction form). (Contributed by NM, 17-Aug-2018.) (Proof shortened by Wolf Lammen, 10-Jul-2019.) Reduce axiom dependencies. (Revised by SN and Sky Winter, 23-Oct-2026.)

Hypothesis
nf5di.1
\( \vdash \varphi \rightarrow \Finv x \, \varphi \)
Conclusion
\( \vdash \Finv x \, \varphi \)
Proof
l0
hbe1
nf5di.1
nfrd _
com12 _
eximdh l0 _
l5
pm2.43i _
\( \vdash \exists x \, \varphi \rightarrow \exists x \, \forall x \, \varphi \)
hbe1a
\( \vdash \exists x \, \forall x \, \varphi \rightarrow \forall x \, \varphi \)
syl l5 _
nfi _