Глупый вопрос по теореме дедукции (Мендельсон)

[Sonic86]

Так формулируется теорема дедукции для ИВ в Мендельсоне:

Мендельсон писал(а):

Предложение 1.8. (Теорема дедукции). Если $\Gamma$ - множество формул, $A,B$ - формулы и $\Gamma, A \vdash B$, то $\Gamma, \vdash (A \to B)$.

Однако не утверждается, что верно обратное: если $\Gamma, \vdash (A \to B)$, то $\Gamma, A \vdash B$. Думаю, что это верно:
Док-во: Пусть $\Gamma, \vdash (A \to B)$, докажем, что $\Gamma, A \vdash B$. $\Gamma, A \vdash B$ означает, что есть вывод $B$ из $\Gamma, A$. Построим вывод:
1. $\Gamma$ (гипотеза)
2. $A \to B$ (следует из 1 по условию)
3. $A$ (гипотеза)
4. $B$ (MP из 2. и 3.)
Значит $\Gamma, A \vdash B$.
(ну тупо, конечно, но так надо) (аксиомы не использовал, только MP)

Вот сразу после доказательства идет следствие 1.9 (которое я счел следствием предложения 1.8).

Мендельсон писал(а):

Следствие 1.9. (i)$A \to B, B \to C \vdash A \to C$...
Доказательство (i):
1. $A \to B$ (гипотеза)
2. $B \to C$ (гипотеза)
3. $A$ (гипотеза)
4. $B$ (MP из 1. и 3.)
5. $C$ (MP из 2. и 4.)

Ну и собственно вопрос: я в упор понять не могу, каким образом из теоремы дедукции и 1 и 2 следует 3. И думаю, что 3 следует из 1 и из обратной теоремы дедукции (которую я на всякий случай доказал, чтоб было видно, что доказательство возможно), а теорема дедукции тут вообще не нужна.
Правильно?

[Null]

Ну мы пытаемся доказать $A \to B, B \to C, A \vdash C$, а из этого следует $A \to B, B \to C \vdash A \to C$, прямая теорема о дедукции.

[Sonic86]

Ой! Я тут чушь написал!

[Null]

У вас в следствии доказывают $A \to B, B \to C \vdash A \to C$, значит оно надо.

А мы доказываем $A \to B, B \to C, A\vdash C$ и потом выводим нам нужное.

[Sonic86]

Null в сообщении #537188 писал(а):

У вас в следствии доказывают $A \to B, B \to C \vdash A \to C$, значит оно надо.

А мы доказываем $A \to B, B \to C, A\vdash C$ и потом выводим нам нужное.

Аааа, вот так Действительно, спасибо!

А обратная теорема сама по себе верна?

[Null]

Да.

[Sonic86]

О! Спасибо большое