すいません。間違えました。
訂正。
←の方はmodus ponensより明らかに成り立つ。
→の方はＢ∨¬Ｂが証明可能だからまずＢが証明可能と仮定するとＡ→Ｂは証明可能。
また¬Ｂが証明可能だと仮定すると仮定より¬Ａが証明可能。よって¬Ｂ→¬Ａが証明可能
以上よりＡ→Ｂ証明可能となる。
同様にしてＡ∨¬Ａが証明可能であることを使ってＢ→Ａも証明可能が示される。