Can we eliminate quantifiers in predicate logic

Question

If we have multiple quantifiers on a predicate say something like $ \exists x \forall y \forall z P(x,y,z)$, can we eliminate $ \forall z$ first using the universal elimination or do we have to start elimination always from the leftmost quantifier i.e $\exists x$ here.

I am looking to prove $ \exists x \forall y \forall z P(x,y,z) \vdash \forall z \forall y \exists x P(x,y,z)$ . The only way that seems possible is if I eliminate $z$ and $y$ first and then use universal introduction, but that feels kind of wrong and I am not sure if I can do that. Any help will be appreciated.

Answer 1

We have to start the elimination always from the leftmost quantifier.

Consider the simpler case :

$∃x∀zP(x,z) ⊢ ∀z∃xP(x,z)$;

I'll prove it with Natural Deduction :

1) $∃x∀zP(x,z)$ --- premise

2) $∀zP(a,z)$ --- from 1) : assumed [a] for $\exists$-elim

3) $P(a,b)$ --- from 2) by $\forall$-elim

4) $∃xP(x,b)$ --- from 3) by $\exists$-intro

5) $∃xP(x,b)$ --- from 2) and 4) by $\exists$-elim, discharging [a]

6) $∀z∃xP(x,z)$ --- from 5) by $\forall$-intro.