# Metamath Proof Explorer

## Theorem bj-nnf-alrim

Description: Proof of the closed form of alrimi from modalK (compare alrimiv ). See also bj-alrim . Actually, most proofs between 19.3t and 2sbbid could be proved without ax-12 . (Contributed by BJ, 20-Aug-2023)

Ref Expression
Assertion bj-nnf-alrim ${⊢}Ⅎ\text{'}{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 bj-nnfa ${⊢}Ⅎ\text{'}{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 alim ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
3 1 2 syl9 ${⊢}Ⅎ\text{'}{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$