Suppose $\phi$ is a formula of L. Give a proof in L of the formula $(\phi \rightarrow \phi)$ explaining each step of the proof. Suppose $\phi$ is a formula of L. Give a proof in L of the formula $(\phi \rightarrow \phi)$ explaining each step of the proof.
I have the axioms
(A1) $(\phi \rightarrow ( \psi \rightarrow \phi))$
(A2) $((\phi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi)))$
(A3) $(((\lnot\phi) \rightarrow (\lnot\psi)) \rightarrow (\psi \rightarrow \phi))$
I really struggle to see how to construct a proof like this. I can follow an example but I do not know how to begin my own.
Thanks
 A: (A1) and (A2) are in Elliott Mendelson, Introduction to mathematical logic (4ed - 1997).
This is a copy of Lemma 1.8. : $⊢\varphi → \varphi$ [see Mendelson, page 36] :
(1) $⊢[A→((B→A)→A)]→[(A→(B→A))→(A→A)]$ --- Ax2, with the following substitutions : $A$ in place of $\varphi$, $B→A$ in place of $\psi$ and $A$ in place of $\chi$.
(2) $⊢A→((B→A)→A)$ --- Ax1, with the following substitutions : $A$ in place of $\varphi$ and $B→A$ in place of $\psi$.
(3) $⊢(A→(B→A))→(A→A)$ --- from (1) and (2) by modus ponens
(4) $⊢A→(B→A)$ --- Ax1, with the following substitutions : $A$ in place of $\varphi$ and $B$ in place of $\psi$.
(5) $⊢A→A$ --- from (3) and (4) by modus ponens.
This is schematic; replace $A$ with a formula $\varphi$ whatever, and you will get the following instance of the theorem :


$\vdash \varphi \rightarrow \varphi$.


A: To begin on your own:
It usually helps to take two theorems and derive the most general theorem from those theorems first before trying to look for substitution instances of those theorems.  To clarify the term "most general", (p→(q→p)) is more general than (p→(p→p)) since you can derive (p→(p→p)) from (p→(q→p)) just by substitution, but you can't derive (p→(q→p)) from (p→(p→p)) just by substitution.  You have 3 theorems to start with, and thus you have 3$^2$=9 nine ordered pairs of theorems to start with, each of which may help lead to a theorem.  They are:


*

*[(p→(q→p)),  ((p→(q→r))→((p→q)→(p→r)))]

*[(p→(q→p)),  (((¬p)→(¬q))→(q→p))]

*[(p→(q→p)), (p→(q→p))]

*[((p→(q→r))→((p→q)→(p→r))), (p→(q→p))]

*[((p→(q→r))→((p→q)→(p→r))), ((p→(q→r))→((p→q)→(p→r)))]

*[((p→(q→r))→((p→q)→(p→r))), (((¬p)→(¬q))→(q→p))]

*[(((¬p)→(¬q))→(q→p)), (p→(q→p))]

*[(((¬p)→(¬q))→(q→p)), (((¬p)→(¬q))→(q→p))]

*[(((¬p)→(¬q))→(q→p)), ((p→(q→r))→((p→q)→(p→r)))]


What do you do with one of these 9 pairs of formulas?  Well, let's try to substitute the right formula into the antecedent of the left formula while making sure to apply all substitution of variables uniformly throughout the formula.  If we can do that, the rule of detachment or modus ponens immediately allows us to detach a theorem.  If we can't perform such a substitution, let's try and find a substitution instance of the right formula and the left formula such that we can substitute the (substitution instance of the) right formula into the (substitution instance of the) left formula.  Also, let's keep track of all variables in the consequent which are not in the antecedent.  If we have a variable in the consequent of the left formula which is NOT it's in antecedent, we can freely change it to another variable to get more general formulas.
For example, let's look at pair 3.  [(p→(q→p)), (p→(q→p))]  We can substitute p with (p→(q→p)), thus putting the right formula into the antecedent of the left.  We can also substitute q with r.  Performing these substitutions we obtain
(((p→(q→p))→(r→(p→(q→p)))).  Then since (p→(q→p)) is a theorem, we can detach
(r→(p→(q→p))).
More specifically, with respect to this problem, let's look at 4.  Can we substitute (p→(q→p)) or some substitution instance of it into the antecedent of ((p→(q→r))→((p→q)→(p→r)))?  
The antecedent of ((p→(q→r))→((p→q)→(p→r))).  The antecedent (p→(q→r)) is a more general formula than (p→(q→p)), since if we substitute r with p in (p→(q→r)) we obtain (p→(q→p)).  Thus, we can substitute (p→(q→p)) into the antecedent of ((p→(q→r))→((p→q)→(p→r))), which along with keeping in mind that such a substitution entails substituting "r" with "p" throughout the entire formula, yields
((p→(q→p))→((p→q)→(p→p))).  Since the antecedent of ((p→(q→p))→((p→q)→(p→p))) is also a theorem, we now can detach the consequent 
((p→q)→(p→p)).
Now can we find a formula (p→q) OR a substitution instance of (p→q) which is a theorem such that it's antecedent is a single variable?  Well, we had (r→(p→(q→p))) above.  So, that formula would work, and so would (p→(q→p)).  If you've followed how we derived (r→(p→(q→p))) rather carefully, you hopefully would see that we could derive (s→(r→(p→(q→p)))) or even (a→(b→(c→(d→(e→(f→(g→(r→(p→(q→p)))))))))) and put any of those formulas into the antecedent of ((p→q)→(p→p)), and then deduce (p→p) from any of them.
