Metamath Proof Explorer

Theorem nf5dh

Description: Deduce that x is not free in ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016) df-nf changed. (Revised by Wolf Lammen, 11-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 nf5dh.1 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nf5dh.2 ${⊢}{\phi }\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
3 1 2 alrimih ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
4 nf5-1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
5 3 4 syl ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$