<s>[INST] Prove that this is a valid formula using axioms of propositional logic The question is how to prove using basic axioms this expression:
$$(A \to B) \to ((\lnot C \to A) \to (\lnot C \to B))$$
I have the list of axioms, one of them looks like this: $A \to (B \to A)...$ But I don't understand how to apply this to my expression... 
 [/INST] Start with a premised proof:
$$\begin{array} {rl}
   \text{Premise} :& A \Rightarrow B
\\ \text{Premise} :& \lnot C \Rightarrow A
\\ \text{Premise} :& \lnot C
\\ \text{MP}      :& A
\\ \text{MP}      :& B
\end{array}$$
Then apply deduction theorem:
$$\begin{array} {rl}
   \text{Ax 1}    :& (A \Rightarrow B) \Rightarrow \lnot C \Rightarrow A \Rightarrow B
\\ \text{Ax 2}    :& (\lnot C \Rightarrow A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B
\\ \text{Premise} :& A \Rightarrow B
\\ \text{Premise} :& \lnot C \Rightarrow A
\\ \text{MP}      :& \lnot C \Rightarrow A \Rightarrow B
\\ \text{MP}      :& (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B
\\ \text{MP}      :& \lnot C \Rightarrow B
\end{array}$$
Then apply deduction theorem again:
$$\begin{array} {rl}
   \text{Ax 1}    :& (A \Rightarrow B) \Rightarrow \lnot C \Rightarrow A \Rightarrow B
\\ \text{Ax 2}    :& (\lnot C \Rightarrow A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B
\\ \text{Premise} :& A \Rightarrow B
\\ \text{MP}      :& \lnot C \Rightarrow A \Rightarrow B
\\ \text{MP}      :& (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B
\end{array}$$
Then apply deduction theorem again:
$$\begin{array} {rl}
\\ \text{Ax 2}    :& (\lnot C \Rightarrow A \Rightarrow B) \Rightarrow
\\                 & (\lnot C \Rightarrow A) \Rightarrow
\\                 & \lnot C \Rightarrow B
\\ \text{Ax 1}    :& ((\lnot C \Rightarrow A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B) \Rightarrow 
\\                 & (A \Rightarrow B) \Rightarrow 
\\                 & (\lnot C \Rightarrow A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B
\\ \text{MP}      :& (A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B
\\ \text{Ax 2}    :& ((A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B) \Rightarrow
\\                 &  ((A \Rightarrow B) \Rightarrow \lnot C \Rightarrow A \Rightarrow B) \Rightarrow 
\\                 & (A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B
\\ \text{MP}      :& ((A \Rightarrow B) \Rightarrow \lnot C \Rightarrow A \Rightarrow B) \Rightarrow (A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B
\\ \text{Ax 1}    :& (A \Rightarrow B) \Rightarrow \lnot C \Rightarrow A \Rightarrow B
\\ \text{MP}      :& (A \Rightarrow B) \Rightarrow (\lnot C \Rightarrow A) \Rightarrow \lnot C \Rightarrow B
\end{array}$$
</s>