# Metamath Proof Explorer

## Theorem nfim1

Description: 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)

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

### Proof

Step Hyp Ref Expression
1 nfim1.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfim1.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 nf3 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\vee \forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)$
4 1 3 mpbi ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\vee \forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)$
5 nftht ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
6 2 sps ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
7 5 6 nfimd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
8 pm2.21 ${⊢}¬{\phi }\to \left({\phi }\to {\psi }\right)$
9 8 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
10 nftht ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
11 9 10 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
12 7 11 jaoi ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\vee \forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
13 4 12 ax-mp ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$