Show that $((\phi → \psi)→((\psi→\chi)→(\phi→\chi)))$ is a Theorem of L. Show that $((\phi → \psi)→((\psi→\chi)→(\phi→\chi)))$ is a Theorem of L.
I a previous part of the Q i am asked to state the deduction theorem so I assume i have to use this and the axioms A1, A2, A3, and also Modus Ponens to prove that the formula is a theorem of L.
I am really struggling with doing any question using the axioms to show something is a theorem of L. I can almost work my way through an example, but even then I am confused with why / how certain steps are done.
Could you help me work through this.
Thanks
 A: If you are allowed to appeal to the deduction theorem then this is very easy, and indeed you don't need to make further appeal to any of the axioms (so it just happens that this question can be answered even though you haven't told us which particular axioms A1, A2, A3 in fact are).
For you can show
$$\varphi, (\varphi \to \psi), (\psi \to \chi) \vdash_L \chi$$
using modus ponens twice (OK?). Then one application of the deduction theorem gives you
$$(\varphi \to \psi), (\psi \to \chi) \vdash_L (\varphi \to \chi)$$
(OK?) and a second application gives you
$$(\varphi \to \psi) \vdash_L ((\psi \to \chi) \to (\varphi \to \chi))$$
(OK?). And then what happens if you use the deduction theorem again?
A: So, let's look at "((ϕ→ψ)→((ψ→χ)→(ϕ→χ)))".  It is a conditional.  What is it's antecedent?  (ϕ→ψ).  What is it's consequent?  ((ψ→χ)→(ϕ→χ)).  Thus, if we have the deduction (meta) theorem, if we assume (ϕ→ψ) and can derive ((ψ→χ)→(ϕ→χ)), we can then use the proof procedure outlined by the proof of the deduction theorem to get to ((ϕ→ψ)→((ψ→χ)→(ϕ→χ))).  But, how do we get ((ψ→χ)→(ϕ→χ))?  Well, what is the primary connective for ((ψ→χ)→(ϕ→χ))?  A conditional.  So, what's the antecedent?  (ψ→χ).  What's the consequent?  (ϕ→χ).  Thus, if we can assume (ψ→χ) and derive (ϕ→χ), then we can infer  ((ψ→χ)→(ϕ→χ)) by the derivable rule of conditional introduction, which follows from the deduction theorem.  Note that when trying to prove ((ψ→χ)→(ϕ→χ)), we still had the assumption (ϕ→ψ) in place.  How do we derive (ϕ→χ)?  Well, could we assume the antecedent ϕ and deduce the consequent χ?  In other words... can we do this...
  1 |   (ϕ→ψ) assumption
  2 ||  (ψ→χ) assumption
  3 ||| ϕ     assumption
  .
  .
  .
  x ||| χ     ?

