Theorem nfim1
A closed form of nfim. (Contributed by NM, 2-Jun-1993.) (Revised by
Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen,
2-Jan-2018.) [df-nf] changed. (Revised by Wolf Lammen, 18-Sep-2021.)
Hypotheses
nfim1.1
\( \vdash \Finv x \, \varphi \)
nfim1.2
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \Finv x \, (\varphi \rightarrow \psi) \)
Proof
l0
nfim1.1
\( \vdash \Finv x \, \varphi \)
nf3
\( \vdash \Finv x \, \varphi \leftrightarrow \forall x \, \varphi \vee \forall x \, \neg \varphi \)
l2
mpbi l0 _
\( \vdash \forall x \, \varphi \vee \forall x \, \neg \varphi \)
l3
nftht
nfim1.2
sps _
l6
nfimd l3 _
pm2.21
l8
alimi _
\( \vdash \forall x \, \neg \varphi \rightarrow \forall x \, (\varphi \rightarrow \psi) \)
nftht
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \Finv x \, (\varphi \rightarrow \psi) \)
syl l8 _
jaoi l6 _
\( \vdash \forall x \, \varphi \vee \forall x \, \neg \varphi \rightarrow \Finv x \, (\varphi \rightarrow \psi) \)
ax-mp l2 _