# Metamath Proof Explorer

## Theorem nf3an

Description: If x is not free in ph , ps , and ch , then it is not free in ( ph /\ ps /\ ch ) . (Contributed by Mario Carneiro, 11-Aug-2016)

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

### Proof

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