# Metamath Proof Explorer

## Theorem ral2imi

Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006) Allow shortening of ralim . (Revised by Wolf Lammen, 1-Dec-2019)

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

### Proof

Step Hyp Ref Expression
1 ral2imi.1 ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
2 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)$
3 1 imim3i ${⊢}\left({x}\in {A}\to {\phi }\right)\to \left(\left({x}\in {A}\to {\psi }\right)\to \left({x}\in {A}\to {\chi }\right)\right)$
4 3 al2imi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\psi }\right)\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}}{\psi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\psi }\right)$
6 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\chi }\right)$
7 4 5 6 3imtr4g ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
8 2 7 sylbi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\chi }\right)$