# Metamath Proof Explorer

## Theorem nfifd

Description: Deduction form of nfif . (Contributed by NM, 15-Feb-2013) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypotheses nfifd.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
nfifd.3 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfifd.4 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfifd ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}if\left({\psi },{A},{B}\right)$

### Proof

Step Hyp Ref Expression
1 nfifd.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
2 nfifd.3 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 nfifd.4 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
4 dfif2 ${⊢}if\left({\psi },{A},{B}\right)=\left\{{y}|\left(\left({y}\in {B}\to {\psi }\right)\to \left({y}\in {A}\wedge {\psi }\right)\right)\right\}$
5 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
6 3 nfcrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
7 6 1 nfimd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {\psi }\right)$
8 2 nfcrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
9 8 1 nfand ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {\psi }\right)$
10 7 9 nfimd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {B}\to {\psi }\right)\to \left({y}\in {A}\wedge {\psi }\right)\right)$
11 5 10 nfabdw ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{y}|\left(\left({y}\in {B}\to {\psi }\right)\to \left({y}\in {A}\wedge {\psi }\right)\right)\right\}$
12 4 11 nfcxfrd ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}if\left({\psi },{A},{B}\right)$