prove $(s\implies p)\implies((\neg s\implies p)\implies p)$ prove $(s\implies p)\implies((\neg s\implies p)\implies p)$
rules to use in this proof:
a)$(\neg A\implies \neg B)\implies (B\implies A)$
b)$(A\implies B)\implies(\neg B\implies\neg A)$
c)Deduction Theorem
d)M.Ponens
Proof:
1)$(s\implies p)$..................assumption
2)$(\neg s\implies p)$..................asum
Then i tried to get p but ended no where
So i tried  a different way
1)$(s\implies p)$..................assumption
2)$\neg p$.........................assum
3)$(s\implies p)\implies (\neg p\implies\neg s)$..................by (a)
4)$(\neg p\implies\neg s)$......................by 1,3 m.p
5)$\neg s$....................................by 2,4 m.p
But now i dont know how to get :
$\neg(\neg s\implies p)$
Because then using the d.theorem i will have proved:
$\neg p\implies \neg(\neg s\implies p)$ which by using rule (a) and m.p  will get me the desired result
Can somebody help??
 A: Your two axioms together with Modus Ponens are not sufficient to prove this.  So you are trying to do the impossible!
How do I know this?
Remember that these formal proofs are purely syntactical beasts: all they do is "if you have a statement that looks like such-and-so, you can infer a statement that looks like this-and-that"
So, if we interpret the symbols as intended, then the theorem to be proven is a true statement about logic. However, what if we interpret the symbols and operators completely differently?
Well, suppose that the expressions are algebraic expressions about some domain where there are two objects, $X$ and $O$.
Also suppose that the $\neg$ and $\to$ are operators that work on these objects as provided by the following tables:
\begin{array}{c|c}
p&\neg p\\
\hline
X & O\\
O & X\\
\end{array}
(so note: this is not a truth-table, since we're not working with truth-functions at all in this domain.)
\begin{array}{cc|c}
p&q&p \to q\\
\hline
X & X & X\\
X & O & O\\
O & X & O\\
O & O & X\\
\end{array}
OK, so with these definitions, let's work out the value of the two axioms under each of the different value-combinations of $A$ and $B$:
\begin{array}{cc|ccc|ccc}
A&B&(\neg A \to \neg B)& \to &(B \to A)&(A \to B)&\to&(\neg B \to \neg A)\\
\hline
X & X & X & X & X & X & X & X\\
X & O & O & X & O & O & X & O\\
O & X & O & X & O & O & X & O\\
O & O & X & X & X & X & X & X\\
\end{array}
Hmm, interesting!  Note that no matter the values of $A$ and $B$, the two axioms will always evaluate to $X$.  As such, we can call them '$X$-beasts'
OK, but now notice that when we evaluate both $s$ and $p$ to $X$, the expression of the theorem $(s \to p) \to ((\neg s \to p) \to p)$ evaluates to $(X \to X) \to ((\neg X \to X) \to X) = X \to ((O \to X) \to X) = X \to (O \to X) = X \to O = O$
OK, so the theorem is not an $X$-beast
Finally, note that if you look at the working of the $\to$ function, you find that whenever $P$ has the value of $X$, and $p \to q$ has the value of $X$, then $q$ has the value of $X$ as well, since if $q$ would have the value of $O$, $p \to q$ would have the value of $O$ as well.  What this tells us is that if you have an expression $p$ that is an $X$-beast, and another expression $p \to q$ that is an $X$-beast, then $q$ will have to be an $X$-beast as well.  In other words, if what you start out with are $X$-beasts, then using Modus Ponens, you can only get more $X$-beasts.
In sum, given that the axioms are $X$-beasts, and given that using Modus Ponens I can only derive more $X$-beasts, I cannot derive any thing that is not an $X$-beast.  But we just saw that your theorem is not an $X$-beast. So, your theorem is not derivable.
 And the same is true for the Deduction Theorem: if $p$ is an $X$-beast, and $q$ is an $X$-best, then $p \to q$ will be an $X$-beast as well. 
OK, but what about the Deduction Theorem? Would that help?  Well, let's first point out that it is strange to say that you can use the Deduction Theorem ... when your axioms together with Modus Ponens are not sufficient to give you the Deduction Theorem!  That is, the Deduction Theorem is always a meta-theorem that says something about the capabilities of a system. And yes, for most systems the Deduction Theorem is true. But not for your system!  As DougSpoonwood points out in the comments: If the Deduction Theorem would be true for your system, then it would be able to derive $p \to (q \to p)$.  But it can't!
DougSpoonwood provides a very nice purely syntactical argument for this: with your axioms you can only get statements that contain an even number of atomic statements. And using Modus Ponens: if $\phi$ contains an even number of atomic statements, and $\phi \to \psi$ contains an even number of atomic statements, then $\psi$ will contain an even number of atomic statements as well. So: from your two axioms, and using Modus Ponens, you can never obtain any statement with an odd number of atomic satements. So, you can't infer $p \to (q \to p)$ .. and thus the Deduction Theorem does not hold.
In fact, using this very same argument, you can directly show that your theorem $(s \to p) \to ((\neg s \to p) \to p)$ cannot be inferred from your two axioms plus Modus Ponens either!
One last note: I could have stayed with the domain of logic and truth-values. And if I interpret the $\neg$ as normal, but I interpret the $\to$ as how we normally interpret the $\leftrightarrow$, then you'll find that the axioms are logical tautologies, that by subsequent uses of Modus Ponens and the Deduction theorem I can only get more logical tautologies, but that the theorem is not a logical tautology. So that would have worked as a demonstration as well. But I use two 'nonsense' objects $X$ and $O$ to drive the point home that there is a big difference between 'mere' syntactical symbol-manipulation and what it all means.
A: I think the simplest way would be to build the truth table for this expression, but here is a sequence of logical equivalences:
$$ (s\rightarrow p)\rightarrow ((\neg s \rightarrow p) \rightarrow p)$$
$$ \neg (s\rightarrow p) \vee ((\neg s \rightarrow p) \rightarrow p)$$
$$ \neg (\neg s\vee  p) \vee (( s \vee p) \rightarrow p)$$
$$  ( s \wedge \neg  p) \vee (\neg ( s \vee p) \vee p)$$
$$  ( s \wedge \neg  p) \vee ( ( \neg s \wedge \neg p) \vee p)$$
$$  ( s \wedge \neg  p) \vee  ( \neg s \wedge \neg p) \vee p$$
$$  ( (s\vee \neg s) \wedge \neg  p) \vee  p$$
$$ \neg p \vee p$$
A: 1)$(s\implies p)$..................assumption
2)$\neg p$.........................assum
3)$(s\implies p)\implies (\neg p\implies\neg s)$..................by (a)
4)$(\neg p\implies\neg s)$......................by 1,3 m.p
5)$\neg s$....................................by 2,4 m.p
6)$\neg s\implies p$..............................assum
7)$p$..........................................5,6 m.p
8)$(\neg s\implies p)\implies p$..........................6 to 7 (c)
9)$((\neg s\implies p)\implies p)\implies(\neg p\implies\neg(\neg s\implies p))$..by(b)
10)$\neg p\implies\neg(\neg s\implies p)$.......................by8,9 m.p
11)$\neg p\implies\neg(\neg s\implies p)\implies(\neg s\implies p)\implies p$..by(a)
12)$(\neg s\implies p)\implies p$................................by 10,11 m.p
13)$(s\implies p)\implies(\neg s\implies p)\implies p$............by 1 to 12 (c)
