# Metamath Proof Explorer

## Theorem stdpc5t

Description: Closed form of stdpc5 . (Possible to place it before 19.21t and use it to prove 19.21t ). (Contributed by BJ, 15-Sep-2018) (Proof modification is discouraged.)

Ref Expression
Assertion stdpc5t ${⊢}Ⅎ{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 nf5r ${⊢}Ⅎ{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 ${⊢}Ⅎ{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)$