Theorem nf5diOLD

Obsolete version of nf5di as of 23-Oct-2026. (Contributed by NM, 17-Aug-2018.) (Proof shortened by Wolf Lammen, 10-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
nf5diOLD.1
\( \vdash \varphi \rightarrow \Finv x \, \varphi \)
Conclusion
\( \vdash \Finv x \, \varphi \)
Proof
nf5diOLD.1
nf5rd _
pm2.43i _
nf5i _