Metamath Proof Explorer

Theorem nfimd

Description: If in a context x is not free in ps and ch , then it is not free in ( ps -> ch ) . 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)

Ref Expression
Hypotheses nfimd.1 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
nfimd.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
Assertion nfimd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)$

Proof

Step Hyp Ref Expression
1 nfimd.1 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
2 nfimd.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
3 19.35 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 3 biimpi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
5 1 nfrd ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
6 2 nfrd ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
7 5 6 imim12d ${⊢}{\phi }\to \left(\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)\right)$
8 19.38 ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)$
9 4 7 8 syl56 ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)\right)$
10 9 nfd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)$