# Metamath Proof Explorer

## Theorem ralrimivvva

Description: Inference from Theorem 19.21 of Margaris p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014)

Ref Expression
Hypothesis ralrimivvva.1 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\wedge {z}\in {C}\right)\right)\to {\psi }$
Assertion ralrimivvva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 ralrimivvva.1 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\wedge {z}\in {C}\right)\right)\to {\psi }$
2 1 3anassrs ${⊢}\left(\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {y}\in {B}\right)\wedge {z}\in {C}\right)\to {\psi }$
3 2 ralrimiva ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {y}\in {B}\right)\to \forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\psi }$
4 3 ralrimiva ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\psi }$
5 4 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\psi }$