# Metamath Proof Explorer

## Theorem al2im

Description: Closed form of al2imi . Version of alim for a nested implication. (Contributed by Alan Sare, 31-Dec-2011)

Ref Expression
Assertion al2im ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 alim ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)\right)$
2 alim ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {\chi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
3 1 2 syl6 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)\right)$