# Metamath Proof Explorer

## Theorem 3reeanv

Description: Rearrange three restricted existential quantifiers. (Contributed by Jeff Madsen, 11-Jun-2010)

Ref Expression
Assertion 3reeanv ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 r19.41v ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
2 reeanv ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
3 2 anbi1i ${⊢}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)↔\left(\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 1 3 bitri ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)↔\left(\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
5 df-3an ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\wedge {\chi }\right)$
6 5 2rexbii ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\wedge {\chi }\right)$
7 reeanv ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\wedge {\chi }\right)↔\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
8 6 7 bitri ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
9 8 rexbii ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
10 df-3an ${⊢}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)↔\left(\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
11 4 9 10 3bitr4i ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$