Помогите разобраться с исчислением высказываний. Есть пример:

К сожалению у меня только пока мысли по его решению:
Преобразуем тождесто в

. Так же тут можно применить теорему дедукции

.
Еще есть мысли, что согласно вот этой теореме

, можно найти некую

выводимую из первой и второй части тождества.
Следовательно используя секвенции мне надо из

вывести

или некую третью формулу. Вот тут и начинаются проблемы, я не могу понять: по какому признаку мне выбирать секвенции и аксиомы? С чего начать? Правильно ли я вообще думаю?
P.S.как упростить и построить таблицу истинности знаю, но этого и не требуется(( Хочется научится именно ив.