# Metamath Proof Explorer

## Theorem alrimdd

Description: Deduction form of Theorem 19.21 of Margaris p. 90, see 19.21 . (Contributed by Mario Carneiro, 24-Sep-2016)

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

### Proof

Step Hyp Ref Expression
1 alrimdd.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 alrimdd.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 alrimdd.3 ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
4 2 nf5rd ${⊢}{\phi }\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
5 1 3 alimd ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
6 4 5 syld ${⊢}{\phi }\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$