Транзитивностью связки называется теорема КИВ:

(A B) ((B C) (A C))

Похоже на Imp2 или Imp2', только проще. Используем МТД, чтобы доказать эту теорему. На этот раз у нас пока нет подходящей формулы, для которой можно было бы "подвигать значок" , так что нам эту формулу придется сперва получить. Тем не менее, мы можем попробовать подвигать значок просто для того, чтобы понять, какие гипотезы нам могут понадобится. Этот метод будем называть "предварительным передвиганием". Он не входит в доказательство, это - просто способ поиска решения.

(A B) ((B C) (A C))

A B (B C) (A C)

A B, B C A C

A B, B C, A C     (1)

Вот предположительно (подчеркиваю: предположительно!) нам понадобятся эти гипотезы: A B, B C, A. Но только если мы докажем, что и в самом деле из этих гипотез можно вывести формулу C. Попробуем (с этого места пойдет уже доказательство):

1)	A, A B	B	// MP
2)	B, B C	C	// MP

Довольно просто - всего два шага. Тем самым мы доказали формулу (1). Осталось только передвинуть значок обратно в крайнее левое положение:

A B, B C, A C    (1)

A B, B C A C

A B (B C) (A C)

(A B) ((B C) (A C))

Теорема о транзитивности доказана.