Theorem nfim

If \( x \) is not free in \( \varphi \) and \( \psi \), then it is not free in \( \varphi \rightarrow \psi \). Inference associated with nfimt. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) [df-nf] changed. (Revised by Wolf Lammen, 17-Sep-2021.)

Hypotheses
nfim.1
\( \vdash \Finv x \, \varphi \)
nfim.2
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \Finv x \, (\varphi \rightarrow \psi) \)
Proof
l0
nfim.1
\( \vdash \Finv x \, \varphi \)
l1
nfim.2
\( \vdash \Finv x \, \psi \)
nfimt
\( \vdash \Finv x \, \varphi \wedge \Finv x \, \psi \rightarrow \Finv x \, (\varphi \rightarrow \psi) \)
mp2an l0 l1 _