# Metamath Proof Explorer

## Theorem nf3and

Description: Deduction form of bound-variable hypothesis builder nf3an . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 16-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 }$
nfand.3 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\theta }$
Assertion nf3and ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\wedge {\theta }\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 nfand.3 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\theta }$
4 df-3an ${⊢}\left({\psi }\wedge {\chi }\wedge {\theta }\right)↔\left(\left({\psi }\wedge {\chi }\right)\wedge {\theta }\right)$
5 1 2 nfand ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)$
6 5 3 nfand ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left({\psi }\wedge {\chi }\right)\wedge {\theta }\right)$
7 4 6 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\wedge {\theta }\right)$