построить вывод формул в ИВ

[ShMaxG]

Помогите пожалуйста построить вывод формулы в исчислении высказываний:

\[ \left( {B \to C} \right) \to \left( {\left( {A \vee B} \right) \to \left( {A \vee C} \right)} \right) \]

.

Аксиоматика такая:

\[ \begin{gathered} 1.A \to \left( {B \to A} \right) \hfill \\ 2.\left( {A \to \left( {B \to C} \right)} \right) \to \left( {\left( {A \to B} \right) \to \left( {A \to C} \right)} \right) \hfill \\ 3.\left( {\neg B \to \neg A} \right) \to \left( {\left( {\neg B \to A} \right) \to B} \right) \hfill \\ \end{gathered} \]

Вообще, что значит построить вывод формулы? Я так понимаю, что, например, теорему дедукции использовать нельзя, потому что теорема дедукции дает некий критерий, когда формула выводима, но не строит сам вывод. А построить вывод, это значит использовать только аксиомы и правило вывода.

Правило вывода - modus ponens.