propositional logic homework problems Having some trouble with a couple of problems in my metalogic homework. We are using an axiomatic system with the following axioms:

$\vdash B\rightarrow(A\rightarrow B)$
$\vdash (\neg A\rightarrow B)\rightarrow((\neg A\rightarrow \neg
B)\rightarrow A$
$\vdash (A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow
B)\rightarrow (A\rightarrow C))$

We are also allowed to use Modus Ponens in our derivations. 
I'm having trouble showing the following (note that the only symbols part of our language are parentheses, negations, arrows, and letters):


*

*$\{x, \neg y\}\vdash \neg(x\rightarrow y)$

*$\vdash x\leftrightarrow x$ which is the same as $\vdash \neg((x\rightarrow x)\rightarrow \neg(x\rightarrow x))$

*$\{x, y\} \vdash x\wedge y $ which is the same as $\{x, y\} \vdash \neg(x\rightarrow \neg y)$


I also proved many of the excercises, whose answers I can use in all my derivations:

I'm still not completely comfortable with the deduction theorem and I'm sure that I could possibly abuse it to solve (2) and (3). Thanks for any help. 
 A: We assume as only connective the conditional ($\rightarrow$).
We assume also the propositional constant $\bot$ (falsum or absurdity; we can think to it also as a $0$-place connective), and we define the negation of $p$ in this way : $\lnot p$ is $p \rightarrow \bot$.
The other connectives are defined as usual : $p \land q$ is $\lnot (p \rightarrow \lnot q)$, $p \lor q$ is $\lnot p \rightarrow q$ and $p \leftrightarrow q$ is $(p \rightarrow q) \land (q \rightarrow p)$.
1) We will use the Deduction Theorem, i.e. 

if $\Gamma \cup \{ A \} \vdash B$, then $\Gamma \vdash A \rightarrow B$.

We have that :
$\{ x, x \rightarrow y \} \vdash y$ --- by modus ponens
So that :
$\vdash x \rightarrow ((x \rightarrow y ) \rightarrow y)$ --- by DT twice.
Now we will use Transitivity, an we apply it to:
$\vdash x \rightarrow [(x \rightarrow y) \rightarrow y]$  --- it is $A \rightarrow B$ 
$\vdash [(x \rightarrow y) \rightarrow y] \rightarrow [\lnot y \rightarrow \lnot (x \rightarrow y)]$ --- by Lemma 2.3(b), with DT --- it is $B \rightarrow C$
So we have :
$\vdash x \rightarrow [\lnot y \rightarrow \lnot (x \rightarrow y)]$ --- it is $A \rightarrow C$.
Now we apply modus ponens twice :

$\{ x, \lnot y \} \vdash \lnot (x \rightarrow y)$.

3) Using the definition of $x \land y$ as $\lnot(x \rightarrow \lnot y)$, from 1) , with $\lnot y$ in place of $y$ and using Double Negation, we have :

$\{ x, y \} \vdash \lnot (x \rightarrow \lnot y)$.

2) Using the definition of 
$x \leftrightarrow x$ as $(x \rightarrow x) \land (x \rightarrow x)$, 
and using the definition of 
$x \land y$ as $\lnot(x \rightarrow \lnot y)$ 
we have that : 
$x \leftrightarrow x$ is $\lnot [(x \rightarrow x) \rightarrow \lnot (x \rightarrow x)]$.
Now the derivation :
using Axiom 2, (1a) and Transitivity, we have :
$\vdash (A \rightarrow B) \rightarrow ((A \rightarrow \lnot B) \rightarrow \lnot A)$
putting $A$ in place of $B$ we have :
$\vdash (A \rightarrow A) \rightarrow ((A \rightarrow \lnot A) \rightarrow \lnot A)$.
Using Example 2 (i.e.$\vdash A \rightarrow A$) we finally have, by modus ponens :
$\vdash ((A \rightarrow \lnot A) \rightarrow \lnot A)$.
This in turn gives us :
$\vdash [(x \rightarrow x) \rightarrow \lnot (x \rightarrow x)] \rightarrow \lnot (x \rightarrow x)$
Using Lemma 2.3(b) we have :
$\vdash \lnot \lnot (x \rightarrow x) \rightarrow \lnot [(x \rightarrow x) \rightarrow \lnot (x \rightarrow x)]$
Using 1(a) and Transitivity, we have :
$\vdash (x \rightarrow x) \rightarrow \lnot [(x \rightarrow x) \rightarrow \lnot (x \rightarrow x)]$
Now apply modus ponens using Example 2 (i.e. $\vdash x \rightarrow x$) to get :

$\vdash \lnot [(x \rightarrow x) \rightarrow \lnot (x \rightarrow x)]$ that is $x \leftrightarrow x$.

