Здравствуйте! Помогите догадаться как решать это)

Можно пользоваться теоремой дедукции, правилом modus ponens и тремя аксиомами:
A1.

A2.

A3.

Я не могу найти нормальные примеры по этой теме и не понимаю откуда что берется, сижу голову ломаю второй день. Вот до чего додумался:
По теореме дедукции получаем последовательно две гипотезы:
1.
2.

Следующий шаг (не знаю насколько верный):
Берем 2 аксиому(из тех, что выше) с заменой:
1.A на

2.В на

3.С на B.
Не уверен, что можно делать такие замены, но правил и исключений опять же не нашел нигде.
Остается только как то получить

и дальше по правилу mp получить то, что нужно вывести. Заранее спасибо за помощь)
