Theorem nfimd
If in a context \( x \) is not free in \( \psi \) and \( \chi \), then it is not
free in \( \psi \rightarrow \chi \). Deduction form of nfim. (Contributed by
Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen,
30-Dec-2017.) [df-nf] changed. (Revised by Wolf Lammen, 18-Sep-2021.)
Eliminate curried form of nfimt. (Revised by Wolf Lammen,
10-Jul-2022.)
Hypotheses
nfimd.1
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
nfimd.2
\( \vdash \varphi \rightarrow \Finv x \, \chi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, (\psi \rightarrow \chi) \)
Proof
19.35
l1
biimpi _
\( \vdash \exists x \, (\psi \rightarrow \chi) \rightarrow \forall x \, \psi \rightarrow \exists x \, \chi \)
nfimd.1
l3
nfrd _
nfimd.2
nfrd _
l6
imim12d l3 _
\( \vdash \varphi \rightarrow (\forall x \, \psi \rightarrow \exists x \, \chi) \rightarrow \exists x \, \psi \rightarrow \forall x \, \chi \)
19.38
\( \vdash (\exists x \, \psi \rightarrow \forall x \, \chi) \rightarrow \forall x \, (\psi \rightarrow \chi) \)
syl56 l1 l6 _
nfd _