Propositional Logic: Proof involving only the symbols $\{\rightarrow,F \}$ I feel like I literally tried everything. I'm exhausted, and could really use some help.
I was instructed to prove some logic proposition using only the symbols $\{\rightarrow,F \}$.
Let me first describe the proof system I'm using.
It is quite long, so please bare with me, or skip ahead if the staff looks familiar to you.  

The propositional proof system is the following:  
The axioms (schemes) are:
$A_1: \hspace{10pt}(\varphi\rightarrow(\psi\rightarrow\varphi))$
$A_2: \hspace{10pt}((\varphi\rightarrow(\psi\rightarrow\eta))\rightarrow((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)))$
$A_3: \hspace{10pt}(((\varphi\rightarrow F)\rightarrow F)\rightarrow\varphi)$  
(I think they called Lyndon Axioms...)
The inference rule is Modus Ponens, namely; given:
$\varphi\rightarrow\psi$
$\varphi$
We can conclude $\psi$.   

As a quick example, given $\Sigma=\{F\}$ let me show how I'll prove $P$. Meaning, I'll show $\Sigma \vdash P$:  
(1) $F$ (assumption)
(2) $(F\rightarrow ((P\rightarrow F)\rightarrow F))$  (instantiating $A_1$ with $\varphi=F$ and $\psi=(P\rightarrow F)$)
(3) $((P\rightarrow F)\rightarrow F)$ (Modus Ponens of (1) and (2))
(4) $(((P\rightarrow F)\rightarrow F)\rightarrow P)$  (instantiating $A_3$ with $\varphi=P$)
(5) $P$ (Modus Ponens of (3) and (4))   

Now, since even trivial proofs can be insanely long and tedious, I am allowed to use the following four rules:  
1. The Deduction Rule:
$\Sigma\vdash \varphi\rightarrow \psi\iff\Sigma\cup\{\varphi\}\vdash\psi$  
This rule can make life much easier.
For example, using this rule, this: $\Sigma=\{A\rightarrow(B\rightarrow C)\}\vdash B\rightarrow(A\rightarrow C)$ can be proven real quick.
2. Transitive Rule:
$\{\varphi\rightarrow\psi, \psi\rightarrow \eta\}\vdash \varphi\rightarrow\eta$  
Not much to say, quite an intuitive rule.  
3. Contra-Positive Rule:
$\{\varphi\rightarrow\psi\}\vdash (\psi\rightarrow F)\rightarrow (\varphi\rightarrow F)$  
Also a well known rule.  
4. Proof by Cases:
If $\Sigma\cup\{\varphi\}\vdash \psi$ and $\Sigma\cup\{\varphi\rightarrow F\}\vdash \psi$ then $\Sigma\vdash \psi$  
This is also intuitive, if you think about it...
My way of understanding it is: If you can prove something with $\varphi$ and you can also prove it with $\neg \varphi$, then it must be that you can prove it regardless of what $\varphi$ is. In some sense, it does not contribute anything.  

Now, going back to my problem, this is what I need to prove:
Consider $\Sigma$:
$\Sigma=\{$
(1) $(D\wedge \neg Y)\rightarrow H$
(2) $H\rightarrow (H\wedge D)\vee(H\wedge Y)$
(3) $\neg (D\wedge H)$
(4) $D\vee H\vee Y$
$\}$
I need to prove $\Sigma\vdash Y$.  
So first, I translated it to propositions over $\{\rightarrow,F\}$:  
(1) $(((D\rightarrow Y)\rightarrow F)\rightarrow H)$
(2) $(H\rightarrow((H\rightarrow(D\rightarrow F))\rightarrow ((H\rightarrow(D\rightarrow Y))\rightarrow F)))$
(3) $(D\rightarrow (H\rightarrow F))$
(4) $((((D\rightarrow F)\rightarrow H)\rightarrow F)\rightarrow Y)$  
Obviously, there are plenty of ways to translate this propositions, and I'm wondering if it'll be easier to prove with some other translation.  
From this group of four propositions, I need to prove $Y$.
I really tried a lot of ways to attack this problem, but it seems that no matter what I try, I keep getting back to the same point - meaning inferring staff I already have as assumptions.  
For example, I tried to use "Proof By Cases"; to prove that $\Sigma\cup \{H\}\vdash Y$ and also that $\Sigma\cup \{H\rightarrow F\}\vdash Y$, but this led me nowhere.
I tried to use the axioms: arbitrarily instantiating schemes to see if I can infer anything new, but this quickly became exhausting, as the propositions grew very long, very fast.
I tried to find how can the Induction Rule be used, but couldn't.
I even tried to prove this using the original $\Sigma$, and then work my way back to the $\{\rightarrow,F\}$ symbols, with no luck.
Is this really a non-trivial task, or am I missing something here?  
I will very appreciate any comment, thanks for reading through this long post.
 A: I'd suggest proving $\Sigma\vdash D\to Y$ and $\Sigma\vdash H\to Y$ (and $\Sigma\vdash Y\to Y$), then using (4).
Here's a proof of $\Sigma\vdash D\to Y$, first in a "friendly" form, then the (fairly mechanical) translation to a form using just the tools you've listed.
Friendly form:  Suppose $D$.  Suppose further that not $Y$.  By (1), $H$ would follow.  But then $D$ and $H$ are both true, contrary to (3).  Therefore our assumption that not $Y$ is false, so $Y$ is true.  We supposed $D$ and proved $Y$; therefore $D\to Y$.
Using just available tools: First I show that $\Sigma\cup\{D,Y\to F\}\vdash F$.
\begin{align*}
&\text{a.} && D &&\text{assumption} \\
&\text{b.} && D\to(Y\to F)\to H &&\text{alternative translation of (1)} \\
&\text{c.} && (Y\to F)\to H &&\text{modus ponens, b & a} \\
&\text{d.} && Y\to F &&\text{assumption} \\
&\text{e.} && H &&\text{modus ponens, c & d} \\
&\text{f.} && D\to (H\to F) &&\text{your translation of (3)} \\
&\text{g.} && H\to F &&\text{modus ponens, f & a}\\
&\text{h.} && F &&\text{modus ponens, g & e}
\end{align*}
Now we proceed:
\begin{align*}
&\text{p.} & \Sigma\cup\{D,Y\to F\} &\vdash F && \text{proof above} \\
&\text{q.} & \Sigma\cup\{D\} &\vdash (Y\to F)\to F && \text{deduction theorem} \\
&\text{r.} & \Sigma\cup\{D\} &\vdash Y && \text{$A_3$ & modus ponens} \\
&\text{s.} & \Sigma &\vdash D\to Y && \text{deduction theorem}
\end{align*}
A: My problem was insisting on the above translation. Although I was aware that other translations are also possible, I didn't think it will have such a dramatic effect on the proof stages. This was important since, as I mentioned above, even a seemingly trivial proof - using only the axioms - can be painful.
Another problem I had is that it didn't occur to me that there is no restriction on how many time to use the Proof by Cases in my proof, and as I will demonstrate below, that was the key.   

An alternative translation to $\Sigma$ can be:
\begin{align*}
&(1) &&D\rightarrow ((H\rightarrow F)\rightarrow Y)\\
&(2) &&(D\rightarrow F)\rightarrow (H\rightarrow Y)\\
&(3) &&D\rightarrow (H\rightarrow F)\\
&(4) &&(D\rightarrow F)\rightarrow ((H\rightarrow F)\rightarrow Y)
\end{align*}
Using proof by cases, I'll show $\Sigma\cup\{D\}\vdash Y$ and $\Sigma\cup\{D\rightarrow F\}\vdash Y$:  
Case 1: $\Sigma\cup\{D\}\vdash Y$
\begin{align*}
&(5) && D &&  \text{assumption} \\
&(6) && H\rightarrow F &&  \text{MP of (3) and (5)} \\
&(7) && (H\rightarrow F)\rightarrow Y &&  \text{MP of (1) and (5)} \\
&(8) && Y &&  \text{MP of (6) and (7)} \\
\end{align*}
Case 2: $\Sigma\cup\{D\rightarrow F\}\vdash Y$
Again, using Proof By Cases, we split the case to two cases.
Denote $\Sigma\,'=\Sigma\cup \{D\rightarrow F\}$, I'll show $\Sigma\,'\cup\{H\}\vdash Y$ and $\Sigma\,'\cup\{H\rightarrow F\}\vdash Y$.
Case 2.1: $\Sigma\,'\cup\{H\}\vdash Y$
\begin{align*}
&(6) && H &&  \text{assumption} \\
&(7) && H\rightarrow Y &&  \text{MP of (2) and (5)} \\
&(8) && Y &&  \text{MP of (6) and (7)} \\
\end{align*}
Case 2.2: $\Sigma\,'\cup\{H\rightarrow F\}\vdash Y$
\begin{align*}
&(6) && H\rightarrow F &&  \text{assumption} \\
&(7) && (H\rightarrow F)\rightarrow Y &&  \text{MP of (4) and (5)} \\
&(8) && Y &&  \text{MP of (6) and (7)} \\
\end{align*}  
Thus I conclude $\Sigma\vdash Y$.
