# Metamath Proof Explorer

## Theorem ralrimd

Description: Inference from Theorem 19.21 of Margaris p. 90. (Restricted quantifier version.) (Contributed by NM, 16-Feb-2004)

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

### Proof

Step Hyp Ref Expression
1 ralrimd.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 ralrimd.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 ralrimd.3 ${⊢}{\phi }\to \left({\psi }\to \left({x}\in {A}\to {\chi }\right)\right)$
4 1 2 3 alrimd ${⊢}{\phi }\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\chi }\right)\right)$
5 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\chi }\right)$
6 4 5 syl6ibr ${⊢}{\phi }\to \left({\psi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }\right)$