Use the auxiliary variable metatheorem to proof

Question

Use the auxiliary variable metatheorem to show that $$ \vdash (\exists x)(A \land B \land C) \rightarrow (\exists x)(A \rightarrow C \rightarrow B)$$

My answer : By using the deduction theorem we have

$$ (\exists x)(A \land B \land C) \vdash(\exists x)(A \rightarrow C \rightarrow B) $$

(1) $ (\exists x)(A \land B \land C) $ $<hypothesis>$

(2) $ (A \land B \land C)[x := z] $ < auxiliary hypothesis associated with 1,z is fresh>

(3) $ A[x := z] \land B[x :=z] \land C[x := z] $ < definition of substitution (2) >

And i couldn't continue.

Answer 1

After (3) you must use property of $\land$ to "rearrange" $A \land B \land C$ as $A \land C \land B$, and the tautology :

$[(A \land C) \land B] \rightarrow [(A \rightarrow C) \rightarrow B]$.

In this way, you have :

$(A \land B \land C)[x:=z] \vdash (A[x:=z] \rightarrow C[x:=z] \rightarrow B[x:=z])$

and thus :

$(A \land B \land C)[x:=z] \vdash (A \rightarrow C \rightarrow B)[x:=z]$.

With 6.5.1 Theorem. $\vdash A[x := t] \rightarrow (\exists x)A$

we obtain :

$(A \land B \land C)[x:=z] \vdash (\exists x)(A \rightarrow C \rightarrow B)$.

Now we need Auxiliary Variable Metatheorem, and specifically [see page 181] :

6.5.8 Corollary. Assume that $A[x := z] \vdash B$, where $z$ is fresh with respect to $(\exists x)A$ and $B$. Then $(\exists x)A \vdash B$ as well.

You have chosen $z$ "fresh" with respect to $(\exists x)(A \land B \land C)$, and $z$ is not present in the conclusion; thus the Corollary applies and we conclude :

$(\exists x)(A \land B \land C) \vdash (\exists x)(A \rightarrow C \rightarrow B)$.

Finally we use Deduction Theorem to obtain :

$\vdash (\exists x)(A \land B \land C) \rightarrow (\exists x)(A \rightarrow C \rightarrow B)$.