# Metamath Proof Explorer

## Theorem nfand

Description: If in a context x is not free in ps and ch , then it is not free in ( ps /\ ch ) . (Contributed by Mario Carneiro, 7-Oct-2016)

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

### Proof

Step Hyp Ref Expression
1 nfand.1 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
2 nfand.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
3 df-an ${⊢}\left({\psi }\wedge {\chi }\right)↔¬\left({\psi }\to ¬{\chi }\right)$
4 2 nfnd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬{\chi }$
5 1 4 nfimd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to ¬{\chi }\right)$
6 5 nfnd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\left({\psi }\to ¬{\chi }\right)$
7 3 6 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)$