# Metamath Proof Explorer

## Theorem r3al

Description: Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995) (Proof shortened by Wolf Lammen, 30-Dec-2019)

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

### Proof

Step Hyp Ref Expression
1 r2al ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 19.21v ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({z}\in {C}\to {\phi }\right)\right)↔\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {C}\to {\phi }\right)\right)$
3 df-3an ${⊢}\left({x}\in {A}\wedge {y}\in {B}\wedge {z}\in {C}\right)↔\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}\in {C}\right)$
4 3 imbi1i ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\wedge {z}\in {C}\right)\to {\phi }\right)↔\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}\in {C}\right)\to {\phi }\right)$
5 impexp ${⊢}\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}\in {C}\right)\to {\phi }\right)↔\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({z}\in {C}\to {\phi }\right)\right)$
6 4 5 bitri ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\wedge {z}\in {C}\right)\to {\phi }\right)↔\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({z}\in {C}\to {\phi }\right)\right)$
7 6 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\wedge {z}\in {C}\right)\to {\phi }\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({z}\in {C}\to {\phi }\right)\right)$
8 df-ral ${⊢}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {C}\to {\phi }\right)$
9 8 imbi2i ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {C}\to {\phi }\right)\right)$
10 2 7 9 3bitr4ri ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\wedge {z}\in {C}\right)\to {\phi }\right)$
11 10 2albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\wedge {z}\in {C}\right)\to {\phi }\right)$
12 1 11 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {C}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {y}\in {B}\wedge {z}\in {C}\right)\to {\phi }\right)$