I have Cut Elimination and the Deduction Theorem as tools as well as three axioms: PL1, PL2 and PL3 (Sider).I also have the following tools.
Weakening: $\phi \vdash (\psi \rightarrow \phi). $
The MP Technique: $\phi \rightarrow (\psi \rightarrow \chi), \phi\rightarrow \psi \vdash \phi \rightarrow \chi.$
Transitivity: $\phi \rightarrow \psi, \psi \rightarrow \chi \vdash \phi \rightarrow \chi$
Contraposition: $\neg\psi \rightarrow \neg\phi\vdash \phi \rightarrow \psi,$ and; $\phi \rightarrow \psi \vdash \neg\psi \rightarrow \neg\phi$
Ex Falso Quodlibet: $\phi, \neg\phi \vdash \psi$
Negated Conditional: $\neg(\phi \rightarrow \psi) \vdash \phi$ and $\neg(\phi \rightarrow \psi) \vdash \psi$
Excluded Middle MP: $\phi \rightarrow \psi, \neg\phi\rightarrow\psi \vdash \psi$
I need to show that $\phi \rightarrow ((\phi \rightarrow \psi) \rightarrow \psi).$
Does anyone have any general strategy tips for going about axiomatic proofs like this? For example, in doing proofs via natural deduction or trees there are strategies to employ (e.g., always apply a rule for an existential claim first, save discharging universal claims for last, etc.).
I'm worried that the only way I con complete these proofs is by brute force which seems like it would take forever.