Положим

(modus ponens)
Нет, modus ponens - это вывод

если у нас уже есть

и

(просто определение правила вывода).
Где ошибка?
Ну собственно если для любых

и

, выбираемых независимо,

, то действительно

. Если вы имели в виду что-то другое - попробуйте явно выписать кванторы.
Я специально выписал последовательность переходов со всеми нужными кванторами явно. Какой первый переход вам непонятен?
В 1.13 вводится дополнительное условие для

, используемое при выведении (1.14).
Подстановкой 1.13 в 1.12 мы получаем просто следствие из 1.12. Потом можно подставить что-то другое и получить другое следствие. И этими следствиями можно пользоваться одновременно. Только нужно не забывать, что если в этих следствиях самих остались

- то они верны только для тех

, которые мы подставляли. Но в (1.14)

не осталось, поэтому неважно, что мы туда подставляли.
Попробую привести искусственный пример, больше похожий на происходящее.
Зафиксируем

. Пусть

таково что для любого

выполнено

.
Раз (1) выполнено для любого

, то выполнено и для

. Подставим, получим

. И это уже следствие изначального условия, никак от

не зависящее (

в него вообще не входит).
Теперь подставим

в исходное условие, получим что

выполнено для любого

. Значит в частности выполнено для

. Подставим, получим

.