А, та моя цитата немного о другом. Вот вы фактически получили

. Я говорил о том, что теперь если у нас есть вывод

, мы показываем

, приклеивая к первому выводу второй сразу после (ну, почти приклеивая). Ведь исходно нужно доказать, что одно выводится ттт, когда выводится второе, а не то, что оба выводятся из друг друга. Ну, это формальные заморочки.
Теперь про коммутативность. Мне кажется, начинать нужно с вывода

и дальше применить формулу (1). Верно?
Да. Вообще я надеялся на то, что вы будете использовать высокоуровневые теоремы о выводимости

типа дедукции. Смотрите, как можно управиться с коммутативностью:

, потому что

(акс.) и по теореме дедукции;

, потому что

(акс.) и по теореме дедукции;

, потому что

и теорема дедукции два раза;
осталось поприменять теорему о транзитивности выводимости, и получим

(а потом сделаем замену

— фокус, с ассоциативностью, увы, не проходящий).
Вывод, существование которого будет доказываться всеми этими теоремами, будет практически такой, как у вас получился — длинный и правильный, но не выписывать его явно, по-моему, приятно. Так же можно будет разделаться с ожидаемым

. Так как у вас дальше аналогичные штучки с дизъюнкцией, я бы посоветовал этот путь.
-- Чт май 04, 2017 17:50:45 --такой, как у вас получился — длинный и правильный
Правильность, правда, лучше бы поручать проверять не мне, а какой-нибудь программе…