# Metamath Proof Explorer

## Theorem alrimdh

Description: Deduction form of Theorem 19.21 of Margaris p. 90, see 19.21 and 19.21h . (Contributed by NM, 10-Feb-1997) (Proof shortened by Andrew Salmon, 13-May-2011)

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

### Proof

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