# Metamath Proof Explorer

## Theorem hb3an

Description: If x is not free in ph , ps , and ch , it is not free in ( ph /\ ps /\ ch ) . (Contributed by NM, 14-Sep-2003) (Proof shortened by Wolf Lammen, 2-Jan-2018)

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

### Proof

Step Hyp Ref Expression
1 hb.1 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 hb.2 ${⊢}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 hb.3 ${⊢}{\chi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }$
4 1 nf5i ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
5 2 nf5i ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
6 3 nf5i ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
7 4 5 6 nf3an ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\wedge {\chi }\right)$
8 7 nf5ri ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\wedge {\chi }\right)$