Доказать a→(b→a) (a→b)∧c ⊩ (a∨b) →((a→c) →a)

Упрощаем заданные формулы:
a→(b→a)= a∨b∨a=1. (a→b)∧c = a→b ∨c =a∨b ∨c = ab∨c,
(a∨b) →((a→c) →a)=a∨b ∨((a→c) →a)= ab∨a→c∨a=ab∨a∨c∨a =ab∨ac∨a=
= ab∨ac∨a ∨ c (мы применили правило Блэйка к первому и третьему дизъюнктам)=
=ab∨a ∨ c=ab∨a ∨ c=ab∨a ∨ c∨b= a ∨b∨ c.
Следовательно, нам надо доказать следующую выводимость: 1, ab∨c ⊩ a ∨b∨с.
Пусть логическое следование не выполняется, т.е .
(1∧ab∨c→a∨b∨с≡0,или ab∨c→(a∨b∨с)≡0.
На основании определения операции импликации отсюда следует система логических равенств, которая при их совместности будет указывать на правомерность предположения о невыполнимости логического следования, тогда как их несовместность будет означать, что логическое следование имеет место:
ab∨c=1a∨b∨с=0 .
При с=1 система несовместна