Proof a quantified predicate logic statement I am having trouble really understanding how to prove this 
$$(S(y) \to T(y)) \land S(x) \to (∃x)T(x).$$
My solution so far is:


*

*$S(y) \to T(y)$ ---   Hypothesis

*$S(x)$ ---    Hypothesis

*$T(y)$ --- Modus Ponens of 1 and 2

*$(∃x)T(x)$ --- Existential Generalization of 3
It seems incorrect to me due to the usage of x and y.  Can anyone help with this?
 A: It seems to me that there is a "missing" quantifier in front of $(S(y) \to T(y))$...
You cannot prove the formula :

$(S(y) \to T(y)) ∧ S(x) \to (∃x)T(x)$

because it is not valid.
Consider as domain of the interpretation the set $\mathbb N$ of natural numbers and interpret the two predicates $S(x), T(x)$ as : $(x=0)$ and $(x < o)$ respectively.
With this interpretation the above formula "means" :

$((y=0) \to (y < 0)) ∧ (x=0) \to (∃x)(x < 0)$.

Consider now a variavle assignment $s$ such that $s(x)=0$ and $s(y)=1$; then :

$(((y=0) \to (y < 0)) ∧ (x=0) \to (∃x)(x < 0))[s]$ 

is false, because : $((1=0) \to (1 < 0))$ is true and also : $(0=0)$ is true, while : $\exists x(x < 0)$ is clearly false in $\mathbb N$.
Thus : 


$\mathbb N \nvDash (((y=0) \to (y < 0)) ∧ (x=0) \to (∃x)(x < 0))[s]$ 


and thus, having found an interpretation and a variable assignment such that the formula is not satisfied, we have to conclude that the formula is not valid and thus, by soundness, is not provable.

Note
If we "restore" the formula with an universal quantifier :
$\forall y(S(y) \to T(y)) ∧ S(x) \to (∃x)T(x)$
then your "proof startegy" will work :
1) $\forall y(S(y) \to T(y))$ --- hypothesis
2) $S(x)$ --- hypothesis
3) $S(x) \to T(x)$ --- from 1) by Universal Instantiation
4) $T(x)$ --- Modus Ponens from 2) and 3)

5) $(∃x)T(x)$ --- from 4) by Existential Generalization 

