In this logic primitives include ∃ ∀ → ∧ ∨ ⊥. ~A is A→⊥. Substitution of $a$ for $x$ in A is denoted as A$_x$[$a$]. Rules of inference are modus ponens and ∀-generalization. Deduction theorem is usable. Axioms related to quantifiers are
Q1.∀$x$A→A$_x$[$a$] when $a$ is free for $x$ in A
Q2.A$_x$[$a$]→∃$x$A when $a$ is free for $x$ in A
Q3.∀$x$(A→B)→(A→∀$x$B) when $x$ isn't free in A
Q4.∀$x$(B→A)→(∃$x$B→A) when $x$ isn't free in A
Proving things about ∀ is easier for me, because there are axioms and rules to eliminate and reintroduce ∀. I find difficulty on dealing with ∃. There are no rules to get rid of ∃ and no theorems like (~A→~B)→(B→A) and ~~A→A to convert ∃ into ∀.Any help will be appreciated.
See Intuitionistic logic :
1) $A \to ∃y∃xA$ --- Ax.Q2 twice
2) $∃x∃yA \to ∃y∃xA$ --- from 1) by $∃$-Elimination: From $A(x) → C$, where $x$ does not occur free in $C$, conclude $∃xA(x) → C$.
With your rules, you have to use $∀$-Introduction ("$∀$-generalization") on 1) followed by modus ponens with Ax.Q4 twice.